Def SumSqIn

Modification history

2024-08-09 03:04
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra/Ring/SumsOfSquares, Algebra/Ring/Semireal): name convension (#15621)
Deleted SumSqInView on Github →
2024-07-24 10:24
Mathlib/Algebra/Ring/SumsOfSquares.lean
feat (Algebra/Ring): add `isSemireal` class for commutative rings (#14941) …
Added SumSqInView on Github →