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

• 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

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.

• one_add_ne_zero {s : R} (hs : IsSumSq s) : 1 + s ≠ 0

theorem isSemireal_iff (R : Type u_1) [Add R] [Mul R] [One R] [Zero R] : IsSemireal R ↔ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0

@[deprecated IsSemireal (since := "2024-08-09")]

def isSemireal (R : Type u_1) [Add R] [Mul R] [One R] [Zero R] : Prop

Alias of IsSemireal.

---

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.

Equations

• isSemireal = IsSemireal

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.

@[deprecated IsSemireal.not_isSumSq_neg_one (since := "2024-08-09")]

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

Alias of IsSemireal.not_isSumSq_neg_one.

---

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

instance instIsSemirealOfExistsAddOfLE {R : Type u_1} [LinearOrderedSemiring R] [ExistsAddOfLE R] : IsSemireal R

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