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
• neg_one_not_SumSq : ¬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.neg_one_not_SumSq {R : Type u_1} [AddMonoid R] [Mul R] [One R] [Neg R] [self : isSemireal R] : ¬isSumSq (-1)

instance instIsSemireal (R : Type u_1) [LinearOrderedField R] : isSemireal R

Equations

• ⋯ = ⋯