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

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.

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

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.

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.

@[instance 90]

instance instCharZeroOfIsSemireal (R : Type u_1) [NonAssocRing R] [IsSemireal R] : CharZero R