Commit 2025-01-07 17:42 f79db555

View on Github →

chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)

Make documentation clearer and more concise
Make notation consistent
Make proofs cleaner This PR splits off yet more chore material from #16094 Moves:
sumSq -> AddSubmonoid.sumSq

Estimated changes

Modified Mathlib/Algebra/Ring/Semireal/Defs.lean

Modified Mathlib/Algebra/Ring/SumsOfSquares.lean

modified theorem AddSubmonoid.closure_isSquare

added theorem AddSubmonoid.mem_sumSq

added def AddSubmonoid.sumSq

modified theorem IsSumSq.add

modified theorem IsSumSq.nonneg

modified theorem IsSumSq.sum_mul_self

modified inductive IsSumSq

modified theorem mem_sumSq_of_isSquare

deleted def sumSq