Documentation

RealClosedField.Algebra.Ring.Semireal

Semireal rings #

A semireal ring is a commutative ring (with unit) in which -1 is not a sum of squares.

For instance, linearly ordered rings are semireal, because sums of squares are positive and -1 is not.

Main declaration #

References #

source
class IsSemireal (R : Type u_1) [Add R] [Mul R] [One R] [Zero R] :
Prop

A semireal ring is a commutative ring (with unit) in which -1 is not a sum of squares. We define the predicate IsSemireal R for structures R equipped with a multiplication, an addition, a multiplicative unit and an additive unit.

Instances
    source
    theorem isSemireal_iff (R : Type u_1) [Add R] [Mul R] [One R] [Zero R] :
    IsSemireal R ↔ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0
    source
    theorem IsSemireal.not_isSumSq_neg_one {R : Type u_1} [AddGroup R] [One R] [Mul R] [IsSemireal R] :
    ¬IsSumSq (-1)

    In a semireal ring, -1 is not a sum of squares.

    source
    theorem isSemireal_iff_not_isSumSq_neg_one {R : Type u_1} [AddGroup R] [One R] [Mul R] :
    IsSemireal R ↔ ¬IsSumSq (-1)
    source
    theorem IsSemireal.of_not_isSumSq_neg_one {R : Type u_1} [AddGroup R] [One R] [Mul R] :
    ¬IsSumSq (-1) → IsSemireal R

    Alias of the reverse direction of isSemireal_iff_not_isSumSq_neg_one.

    source
    instance instIsSemirealOfNontrivialOfIsFormallyReal {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] [IsFormallyReal R] :
    IsSemireal R
    source
    instance instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] :
    IsSemireal R

    Linearly ordered semirings with the property a ≤ b → ∃ c, a + c = b (e.g. ℕ) are semireal.

    source
    instance instIsPreorderingSumSqOfIsSemireal {R : Type u_1} [CommRing R] [IsSemireal R] :
    (Subsemiring.sumSq R).IsPreordering
    source
    theorem isSemireal_ofIsPreordering {R : Type u_1} [CommRing R] (P : Subsemiring R) [P.IsPreordering] :
    IsSemireal R
    source
    theorem exists_isPreordering_iff_isSemireal {R : Type u_1} [CommRing R] :
    (∃ (P : Subsemiring R), P.IsPreordering) ↔ IsSemireal R
    source
    theorem IsSemireal.isFormallyReal {F : Type u_2} [Field F] [IsSemireal F] :
    IsFormallyReal F