IsFormallyReal

📁 Source: Mathlib/Algebra/Ring/IsFormallyReal.lean

Statistics

Metric	Count
Definitions sumNonzeroSq, IsFormallyReal, IsSumNonzeroSq	3
Theorems closure_mul_self, coe_sumNonzeroSq, mem_sumNonzeroSq, eq_zero_of_add_left, eq_zero_of_add_right, eq_zero_of_isSumSq_of_neg_isSumSq, instIsReduced, instOfIsStrictOrderedRing, not_isSumNonzeroSq_zero, of_eq_zero_of_eq_zero_of_mul_self_add, of_eq_zero_of_mul_self_of_eq_zero_of_add, add, isSumSq, isSumNonzeroSq_of_ne_zero, isSumNonzeroSq_iff, isSumNonzeroSq_iff_isSumSq	16
Total	19

AddSubsemigroup

Definitions

Name	Category	Theorems
sumNonzeroSq 📖	CompOp	3 math math: coe_sumNonzeroSq, closure_mul_self, mem_sumNonzeroSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_mul_self 📖	mathematical	—	closure AddSemigroup.toAdd AddMonoid.toAddSemigroup setOf AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass sumNonzeroSq	—	closure_eq_of_le mem_closure_of_mem AddMemClass.add_mem instAddMemClass
coe_sumNonzeroSq 📖	mathematical	—	SetLike.coe AddSubsemigroup AddSemigroup.toAdd AddMonoid.toAddSemigroup instSetLike sumNonzeroSq setOf IsSumNonzeroSq AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—
mem_sumNonzeroSq 📖	mathematical	—	AddSubsemigroup AddSemigroup.toAdd AddMonoid.toAddSemigroup SetLike.instMembership instSetLike sumNonzeroSq IsSumNonzeroSq AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—

IsFormallyReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_add_left 📖	mathematical	IsSumSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	eq_zero_of_add_right zero_add
eq_zero_of_add_right 📖	mathematical	IsSumSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	add_zero not_isSumNonzeroSq_zero IsSumNonzeroSq.add isSumNonzeroSq_iff_isSumSq
eq_zero_of_isSumSq_of_neg_isSumSq 📖	mathematical	IsSumSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	eq_zero_of_add_right add_neg_cancel
instIsReduced 📖	mathematical	—	IsReduced MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	isReduced_iff_pow_one_lt not_isSumNonzeroSq_zero
instOfIsStrictOrderedRing 📖	mathematical	—	IsFormallyReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	of_eq_zero_of_mul_self_of_eq_zero_of_add mul_self_eq_zero IsDomain.to_noZeroDivisors IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE add_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add IsSumSq.nonneg
not_isSumNonzeroSq_zero 📖	mathematical	—	IsSumNonzeroSq AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
of_eq_zero_of_eq_zero_of_mul_self_add 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	IsFormallyReal NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	add_zero
of_eq_zero_of_mul_self_of_eq_zero_of_add 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	IsFormallyReal	—	—

IsSumNonzeroSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsSumNonzeroSq AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	IsSumNonzeroSq AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	add_assoc
isSumSq 📖	mathematical	IsSumNonzeroSq AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	IsSumSq AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	IsSumSq.add

IsSumSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSumNonzeroSq_of_ne_zero 📖	mathematical	IsSumSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	IsSumNonzeroSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	isSumNonzeroSq_iff_isSumSq

(root)

Definitions

Name	Category	Theorems
IsFormallyReal 📖	CompData	3 math math: IsFormallyReal.instOfIsStrictOrderedRing, IsFormallyReal.of_eq_zero_of_mul_self_of_eq_zero_of_add, IsFormallyReal.of_eq_zero_of_eq_zero_of_mul_self_add
IsSumNonzeroSq 📖	CompData	7 math math: IsFormallyReal.not_isSumNonzeroSq_zero, AddSubsemigroup.coe_sumNonzeroSq, IsSumSq.isSumNonzeroSq_of_ne_zero, AddSubsemigroup.mem_sumNonzeroSq, isSumNonzeroSq_iff_isSumSq, isSumNonzeroSq_iff, IsSumNonzeroSq.add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSumNonzeroSq_iff 📖	mathematical	—	IsSumNonzeroSq	—	—
isSumNonzeroSq_iff_isSumSq 📖	mathematical	—	IsSumNonzeroSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass IsSumSq	—	IsSumNonzeroSq.isSumSq eq_or_ne MulZeroClass.mul_zero zero_add add_zero

---

← Back to Index