Formally real rings

A ring R is formally real if, whenever ∑ i, x i ^ 2 = 0, in fact x i = 0 for all i.

We define formally real rings in an index-free manner using the inductive predicate IsSumNonzeroSq, which asserts that an element is a finite sum of squares of nonzero elements. A ring is then formally real if ¬ IsSumNonzeroSq 0.

Main declaration

• IsFormallyReal: typeclass stating that a ring is formally real.

inductive IsSumNonzeroSq {R : Type u_1} [Mul R] [Add R] [Zero R] : R → Prop

The property of being a sum of positive squares is defined inductively by: a * a : R is a sum of nonzero squares for all nonzero a, and if s : R is a sum of positive squares, and a ≠ 0, then a * a + s is a sum of positive squares.

• sq {R : Type u_1} [Mul R] [Add R] [Zero R] {a : R} (ha : a ≠ 0) : IsSumNonzeroSq (a * a)
• sq_add {R : Type u_1} [Mul R] [Add R] [Zero R] {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s) : IsSumNonzeroSq (a * a + s)

theorem isSumNonzeroSq_iff {R : Type u_1} [Mul R] [Add R] [Zero R] (a✝ : R) : IsSumNonzeroSq a✝ ↔ (∃ (a : R), a ≠ 0 ∧ a✝ = a * a) ∨ ∃ (a : R) (s : R), a ≠ 0 ∧ IsSumNonzeroSq s ∧ a✝ = a * a + s

theorem IsSumNonzeroSq.add {R : Type u_1} [AddMonoid R] [Mul R] {s₁ s₂ : R} (h₁ : IsSumNonzeroSq s₁) (h₂ : IsSumNonzeroSq s₂) : IsSumNonzeroSq (s₁ + s₂)

theorem IsSumSq.isSumNonzeroSq {R : Type u_1} [AddMonoid R] [Mul R] {s : R} (h : IsSumNonzeroSq s) : IsSumSq s

theorem isSumNonzeroSq_iff_isSumSq {R : Type u_1} [NonUnitalNonAssocSemiring R] {s : R} (hs : s ≠ 0) : IsSumNonzeroSq s ↔ IsSumSq s

theorem IsSumSq.isSumNonzeroSq_of_ne_zero {R : Type u_1} [NonUnitalNonAssocSemiring R] {s : R} (hs : s ≠ 0) : IsSumSq s → IsSumNonzeroSq s

Alias of the reverse direction of isSumNonzeroSq_iff_isSumSq.

class IsFormallyReal (R : Type u_1) [AddCommMonoid R] [Mul R] : Prop

A ring is formally real if, whenever ∑ i, x i ^ 2 = 0, we in fact have x i = 0 for all i.

• not_isSumNonzeroSq_zero : ¬IsSumNonzeroSq 0

theorem IsFormallyReal.of_eq_zero_of_mul_self_of_eq_zero_of_add (R : Type u_1) [AddCommMonoid R] [Mul R] (hz : ∀ {a : R}, a * a = 0 → a = 0) (ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0) : IsFormallyReal R

theorem IsFormallyReal.of_eq_zero_of_eq_zero_of_mul_self_add (R : Type u_1) [NonUnitalNonAssocSemiring R] (h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0) : IsFormallyReal R

instance IsFormallyReal.instOfIsStrictOrderedRing (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] : IsFormallyReal R

instance IsFormallyReal.instIsReduced {R : Type u_1} [Ring R] [IsFormallyReal R] : IsReduced R

theorem IsFormallyReal.eq_zero_of_add_right {R : Type u_1} [NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R} (hs₁ : IsSumSq s₁) (hs₂ : IsSumSq s₂) (h : s₁ + s₂ = 0) : s₁ = 0

theorem IsFormallyReal.eq_zero_of_add_left {R : Type u_1} [NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R} (hs₁ : IsSumSq s₁) (hs₂ : IsSumSq s₂) (h : s₁ + s₂ = 0) : s₂ = 0

theorem IsFormallyReal.eq_zero_of_isSumSq_of_neg_isSumSq {R : Type u_1} [NonUnitalNonAssocRing R] [IsFormallyReal R] {s : R} (h₁ : IsSumSq s) (h₂ : IsSumSq (-s)) : s = 0

instance IsFormallyReal.instIsPointedSumSq {R : Type u_1} [CommRing R] [IsFormallyReal R] : (AddSubmonoid.sumSq R).IsPointed

@[simp]

theorem IsFormallyReal.Subsemiring.sumSq_toAddSubmonoid {T : Type u_2} [CommSemiring T] : (Subsemiring.sumSq T).toAddSubmonoid = AddSubmonoid.sumSq T

instance IsFormallyReal.instIsPointedToAddSubmonoidSumSq {R : Type u_1} [CommRing R] [IsFormallyReal R] : (Subsemiring.sumSq R).toAddSubmonoid.IsPointed