Theorem mem_sumSqIn_of_isSquare

Modification history

2025-01-06 17:01
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra): make more names consistent (#20449) …
Deleted mem_sumSqIn_of_isSquareView on Github →
2024-08-09 03:04
Mathlib/Algebra/Ring/SumsOfSquares.lean
chore(Algebra/Ring/SumsOfSquares, Algebra/Ring/Semireal): name convension (#15621)
Added mem_sumSqIn_of_isSquareView on Github →