Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsSemireal.not_isSumSq_neg_one
Modification history
2025-07-04 10:05
Mathlib/Algebra/Ring/Semireal/Defs.lean
chore: whitespace before `:` (#26727) …
Modified
IsSemireal.not_isSumSq_neg_one
View on Github →
2025-01-16 05:31
Mathlib/Algebra/Ring/Semireal/Defs.lean
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings (#16094) …
Added
IsSemireal.not_isSumSq_neg_one
View on Github →