Commit 2025-06-30 13:28 ce423c4b

View on Github →

feat: miscellaneous parity results (#26496)

Estimated changes

Modified Mathlib/Algebra/Group/Int/Even.lean

added theorem Int.isSquare_sign_iff

Modified Mathlib/Algebra/Order/Ring/Basic.lean

added theorem not_isSquare_of_neg

Modified Mathlib/Algebra/Ring/Int/Parity.lean

added theorem Int.even_sign_iff

added theorem Int.odd_sign_iff