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

• eq_zero_of_sum_eq_zero {s : Multiset R} : (Multiset.map (fun (a : R) => a * a) s).sum = 0 → ∀ a ∈ s, a = 0

theorem IsFormallyReal.eq_zero_of_mul_self {R : Type u_1} [AddCommMonoid R] [Mul R] [IsFormallyReal R] {a : R} : a * a = 0 → a = 0

theorem AddSubmonoid.closure_eq_image_multiset_sum {M : Type u_2} [AddCommMonoid M] (s : Set M) : ↑(closure s) = Multiset.sum '' {m : Multiset M | ∀ x ∈ m, x ∈ s}

theorem isSumSq_iff_exists_sum_mul_self_eq {R : Type u_1} [AddCommMonoid R] [Mul R] {x : R} : IsSumSq x ↔ ∃ (s : Multiset R), (Multiset.map (fun (a : R) => a * a) s).sum = x

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_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 instIsFormallyRealOfIsStrictOrderedRing {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] : IsFormallyReal R

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