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

• IsSemireal: the predicate asserting that a commutative ring R is semireal.

References

• An introduction to real algebra, by T.Y. Lam. Rocky Mountain J. Math. 14(4): 767-814 (1984). lam_1984

theorem isSemireal_iff (R : Type u_1) [AddMonoid R] [Mul R] [One R] [Neg R] : IsSemireal R ↔ 0 ≠ 1 ∧ ¬IsSumSq (-1)

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

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.

• non_trivial : 0 ≠ 1
• not_isSumSq_neg_one : ¬IsSumSq (-1)

theorem IsSemireal.non_trivial {R : Type u_1} [AddMonoid R] [Mul R] [One R] [Neg R] [self : IsSemireal R] : 0 ≠ 1

theorem IsSemireal.not_isSumSq_neg_one {R : Type u_1} [AddMonoid R] [Mul R] [One R] [Neg R] [self : IsSemireal R] : ¬IsSumSq (-1)

@[deprecated IsSemireal]

def isSemireal (R : Type u_1) [AddMonoid R] [Mul R] [One R] [Neg R] : Prop

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

• isSemireal = IsSemireal

@[deprecated IsSemireal.not_isSumSq_neg_one]

theorem isSemireal.neg_one_not_SumSq {R : Type u_1} [AddMonoid R] [Mul R] [One R] [Neg R] [self : IsSemireal R] : ¬IsSumSq (-1)

Alias of IsSemireal.not_isSumSq_neg_one.

instance instIsSemireal (R : Type u_1) [LinearOrderedRing R] : IsSemireal R

Equations

• ⋯ = ⋯