diff --git a/CHANGELOG.md b/CHANGELOG.md
index c84ffcf13dccf721161d58d718f70c7b41bd046d..a2eeab25f7fab89bc7362f7205b09c5e9813a6b2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -160,6 +160,7 @@ s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
 s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
+s/\bgmap_view_persist\b/gmap_view_frag_persist/g
 s/\bghost_map_elem_frac_ne\b/ghost_map_elem_dfrac_ne/g
 # big_sepM renames
 s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 51aefe3a9822be2e03a923e2f30d7dd6d4bd79e3..aa19988e144d0d79306ac1cda20e5f8c426649cd 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -407,7 +407,7 @@ Section lemmas.
     gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
   Proof. apply view_update_auth_persist. Qed.
 
-  Lemma gmap_view_persist k dq v :
+  Lemma gmap_view_frag_persist k dq v :
     gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
     apply view_update_frag=>m n bf Hrel j [df va] /=.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index deb27e7fda5cf44df9296d6027df258879181b24..550d798fe8b9233207b7cbd2cc037cdd94adb0d5 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -114,7 +114,7 @@ Section lemmas.
     k1 ↪[γ] v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
   Proof. apply ghost_map_elem_dfrac_ne. apply: exclusive_l. Qed.
 
-  (** Make an element read-only. *)
+  (** Make a the authorative element read-only. *)
   Lemma ghost_map_auth_persist γ dq m :
     ghost_map_auth γ dq m ==∗ ghost_map_auth γ DfracDiscarded m.
   Proof. unseal. iApply own_update. apply gmap_view_auth_persist. Qed.
@@ -122,7 +122,7 @@ Section lemmas.
   (** Make an element read-only. *)
   Lemma ghost_map_elem_persist k γ dq v :
     k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
-  Proof. unseal. iApply own_update. apply gmap_view_persist. Qed.
+  Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
 
   (** * Lemmas about [ghost_map_auth] *)
   Lemma ghost_map_alloc_strong P m :