diff -r 1b0fc6ceb750 -r 22a137a6de44 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Jan 25 17:08:07 2024 +0000
+++ b/src/HOL/Parity.thy	Thu Jan 25 11:19:03 2024 +0000
@@ -925,7 +925,7 @@
 context linordered_euclidean_semiring
 begin
 
-lemma even_mask_div_iff':
+lemma even_decr_exp_div_exp_iff':
   \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
 proof -
   have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>