Documentation

Mathlib.Algebra.Ring.Semireal.Defs

Semireal rings #

A semireal ring is a non-trivial commutative ring (with unit) in which -1 is not a sum of squares. Note that -1 does not make sense in a semiring.

For instance, linearly ordered fields are semireal, because sums of squares are positive and -1 is not. More generally, linearly ordered semirings in which a ≤ b → ∃ c, a + c = b holds, are semireal.

Main declaration #

References #

theorem isSemireal_iff (R : Type u_1) [AddMonoid R] [Mul R] [One R] [Neg R] :
class IsSemireal (R : Type u_1) [AddMonoid R] [Mul R] [One R] [Neg R] :

A semireal ring is a non-trivial commutative ring (with unit) in which -1 is not a sum of squares. Note that -1 does not make sense in a semiring. Below we define the class IsSemireal R for all additive monoid R equipped with a multiplication, a multiplicative unit and a negation.

Instances
    theorem IsSemireal.non_trivial {R : Type u_1} :
    ∀ {inst : AddMonoid R} {inst_1 : Mul R} {inst_2 : One R} {inst_3 : Neg R} [self : IsSemireal R], 0 1
    theorem IsSemireal.not_isSumSq_neg_one {R : Type u_1} :
    ∀ {inst : AddMonoid R} {inst_1 : Mul R} {inst_2 : One R} {inst_3 : Neg R} [self : IsSemireal R], ¬IsSumSq (-1)
    @[deprecated IsSemireal]
    def isSemireal (R : Type u_1) [AddMonoid R] [Mul R] [One R] [Neg R] :

    Alias of IsSemireal.


    A semireal ring is a non-trivial commutative ring (with unit) in which -1 is not a sum of squares. Note that -1 does not make sense in a semiring. Below we define the class IsSemireal R for all additive monoid R equipped with a multiplication, a multiplicative unit and a negation.

    Equations
    Instances For
      @[deprecated IsSemireal.not_isSumSq_neg_one]
      theorem isSemireal.neg_one_not_SumSq {R : Type u_1} :
      ∀ {inst : AddMonoid R} {inst_1 : Mul R} {inst_2 : One R} {inst_3 : Neg R} [self : IsSemireal R], ¬IsSumSq (-1)

      Alias of IsSemireal.not_isSumSq_neg_one.

      Equations
      • =