Commit 2024-07-24 10:24 60c76bf7

feat (Algebra/Ring): add isSemireal class for commutative rings (#14941) A semireal ring is a non-trivial commutative ring with unit R in which -1 : R is not a sum of squares. We add this notion to Mathlib and prove that linearly ordered fields are semireal rings. We also introduce the type of sums of squares in a type R endowed with an Add R, Zero R and Mul R instances. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.