Theorem not_isSquare_of_neg

Modification history

2025-08-14 03:55
Mathlib/Algebra/Order/Ring/Basic.lean
chore(Algebra/Order): generalize (#28227) …
Modified not_isSquare_of_negView on Github →
2025-06-30 13:28
Mathlib/Algebra/Order/Ring/Basic.lean
feat: miscellaneous parity results (#26496)
Added not_isSquare_of_negView on Github →