Theorem sq_nonpos_iff

Modification history

2025-08-14 03:55
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
chore(Algebra/Order): generalize (#28227) …
Modified sq_nonpos_iffView on Github →
2025-04-13 02:25
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
chore(*): rename ring type variables (#23939) …
Modified sq_nonpos_iffView on Github →
2025-02-11 15:00
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
feat: add `sq_nonpos_iff` (#21691)
Added sq_nonpos_iffView on Github →