Theorem mem_sumSq_of_isSquare

Modification history

2025-01-16 05:31
Mathlib/Algebra/Ring/SumsOfSquares.lean
feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings (#16094) …
Deleted mem_sumSq_of_isSquareView on Github →
2025-01-07 17:42
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) …
Modified mem_sumSq_of_isSquareView on Github →
2025-01-06 17:01
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra): make more names consistent (#20449) …
Added mem_sumSq_of_isSquareView on Github →