sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: rename Int.sq_nonnneg to Int.sq_nonneg (#12909)

Browse Source 
This PR fixes the typo in `Int.sq_nonnneg`.

Closes #12906.

---------

Co-authored-by: Claude <noreply@anthropic.com>
This commit is contained in:
Bhavik Mehta
2026-03-16 10:52:57 +00:00
committed by GitHub
parent fa9a32b5c8
commit 76e593a52d
1 changed files with 5 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
src/Init/Data/Int/Pow.lean
View File

@@ -118,16 +118,19 @@ theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat =
| succ k ih =>
rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := by
protected theorem sq_nonneg (m : Int) : 0 ≤ m ^ 2 := by
rw [Int.pow_succ, Int.pow_one]
cases m
· apply Int.mul_nonneg <;> simp
· apply Int.mul_nonneg_of_nonpos_of_nonpos <;> exact negSucc_le_zero _
@[deprecated Int.sq_nonneg (since := "2026-03-13")]
protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := Int.sq_nonneg m
protected theorem pow_nonneg_of_even {m : Int} {n : Nat} (h : n % 2 = 0) : 0 ≤ m ^ n := by
rw [← Nat.mod_add_div n 2, h, Nat.zero_add, Int.pow_mul]
apply Int.pow_nonneg
exact Int.sq_nonnneg m
exact Int.sq_nonneg m
protected theorem neg_pow {m : Int} {n : Nat} : (-m)^n = (-1)^(n % 2) * m^n := by
rw [Int.neg_eq_neg_one_mul, Int.mul_pow]