Commit 2025-01-16 05:31 eec581e5

View on Github →

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings (#16094)

Generalise definition of a semireal ring, as discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Formally.20real.20fields
Add facts about multiplicative structure of sums of squares -- preserved under multiplication, form a semiring, set of sums of squares is the semiring generated by the squares.
Add some lemmas to simpset
Update documentation Deletions:
mem_sumSq_of_isSquare (statement changed to IsSquare.isSumSq)

Estimated changes

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

added theorem IsSemireal.not_isSumSq_neg_one

Modified Mathlib/Algebra/Ring/SumsOfSquares.lean

added theorem IsSquare.isSumSq

added theorem IsSumSq.mul

added theorem IsSumSq.mul_self

added theorem IsSumSq.prod

added theorem IsSumSq.rec'

added theorem IsSumSq.sum

added theorem IsSumSq.sum_isSquare

added theorem NonUnitalSubsemiring.closure_isSquare

added theorem NonUnitalSubsemiring.coe_sumSq

added theorem NonUnitalSubsemiring.mem_sumSq

added def NonUnitalSubsemiring.sumSq

added theorem NonUnitalSubsemiring.sumSq_toAddSubmonoid

added theorem Subsemiring.closure_isSquare

added theorem Subsemiring.coe_sumSq

added theorem Subsemiring.mem_sumSq

added def Subsemiring.sumSq

added theorem Subsemiring.sumSq_toNonUnitalSubsemiring

deleted theorem mem_sumSq_of_isSquare