Defs

📁 Source: Mathlib/Algebra/Ring/Semireal/Defs.lean

Statistics

Metric	Count
Definitions IsSemireal	1
Theorems not_isSumSq_neg_one, of_not_isSumSq_neg_one, one_add_ne_zero, instCharZeroOfIsSemireal, instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE, isSemireal_iff, isSemireal_iff_not_isSumSq_neg_one	7
Total	8

IsSemireal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isSumSq_neg_one 📖	mathematical	—	IsSumSq AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toNeg	—	add_neg_cancel one_add_ne_zero
of_not_isSumSq_neg_one 📖	mathematical	IsSumSq AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toNeg	IsSemireal	—	isSemireal_iff_not_isSumSq_neg_one
one_add_ne_zero 📖	—	IsSumSq	—	—	—

(root)

Definitions

Name	Category	Theorems
IsSemireal 📖	CompData	5 math math: IsSemireal.of_not_isSumSq_neg_one, instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE, isSemireal_iff_not_isSumSq_neg_one, IsRealClosed.toIsSemireal, isSemireal_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCharZeroOfIsSemireal 📖	mathematical	—	CharZero AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	charZero_of_inj_zero IsSemireal.one_add_ne_zero Nat.cast_add Nat.cast_one add_comm
instIsSemirealOfIsStrictOrderedRingOfExistsAddOfLE 📖	mathematical	—	IsSemireal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	zero_ne_one' NeZero.charZero_one IsStrictOrderedRing.toCharZero le_antisymm zero_le_one IsStrictOrderedRing.toZeroLEOneClass le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsSumSq.nonneg
isSemireal_iff 📖	mathematical	—	IsSemireal	—	—
isSemireal_iff_not_isSumSq_neg_one 📖	mathematical	—	IsSemireal AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid IsSumSq NegZeroClass.toNeg	—	IsSemireal.not_isSumSq_neg_one

---

← Back to Index