| changeset 71412 | 96d126844adc |
| parent 71408 | 554385d4cf59 |
| child 71413 | 65ffe9e910d4 |
--- a/src/HOL/Euclidean_Division.thy Tue Jan 28 20:26:23 2020 +0100 +++ b/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:37 2020 +0100 @@ -1933,7 +1933,7 @@ by (simp add: of_nat_mod) qed -lemma range_mod_exp: +lemma mask_mod_exp: \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close> proof - have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)