refactor: add _self

leanprover · Nov 26, 2024 · f889a38 · f889a38
1 parent 31deebd
commit f889a38
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
@@ -851,11 +851,11 @@ protected theorem lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n := by
   | zero => exact Nat.zero_lt_one
   | succ _ ih => exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h)
 
-protected theorem lt_two_pow : n < 2 ^ n :=
+protected theorem lt_two_pow_self : n < 2 ^ n :=
   Nat.lt_pow_self Nat.one_lt_two
 
 @[simp]
-protected theorem mod_two_pow : n % 2 ^ n = n :=
+protected theorem mod_two_pow_self : n % 2 ^ n = n :=
   Nat.mod_eq_of_lt Nat.lt_two_pow
 
 @[simp]