Defs

📁 Source: Mathlib/Algebra/Order/Ring/Ordering/Defs.lean

Statistics

Metric	Count
Definitions `RingPreordering`, `HasIdealSupport`, `IsOrdering`, `copy`, `instPartialOrder`, `instSetLike`, `support`, `supportAddSubgroup`, `toSubsemiring`	9
Theorems `smul_mem_support`, `toHasMemOrNegMem`, `toIsPrime`, `coe_copy`, `coe_set_mk`, `coe_support`, `coe_supportAddSubgroup`, `coe_toSubsemiring`, `copy_eq`, `ext`, `ext_iff`, `hasIdealSupport_iff`, `instHasIdealSupportOfHasMemOrNegMem`, `instSubsemiringClass`, `mem_copy`, `mem_mk`, `mem_of_isSquare`, `mem_of_isSquare'`, `mem_support`, `mem_supportAddSubgroup`, `mem_toSubsemiring`, `mul_self_mem`, `neg_one_notMem`, `neg_one_notMem'`, `pow_two_mem`, `supportAddSubgroup_eq`, `toSubsemiring_inj`, `toSubsemiring_injective`	28
Total	37

RingPreordering

Definitions

Name	Category	Theorems
`HasIdealSupport` 📖	CompData	5 math math: `hasIdealSupport_iff`, `instHasIdealSupportOfHasMemOrNegMem`, `instHasIdealSupport`, `instHasIdealSupportOfFactIsUnitOfNat`, `hasIdealSupport_of_isUnit_two`
`IsOrdering` 📖	CompData	2 math math: `isOrdering_iff`, `IsOrdering.mk'`
`copy` 📖	CompOp	3 math math: `copy_eq`, `coe_copy`, `mem_copy`
`instPartialOrder` 📖	CompOp	4 math math: `toSubsemiring_strictMono`, `toSubsemiring_lt_toSubsemiring`, `toSubsemiring_mono`, `toSubsemiring_le_toSubsemiring`
`instSetLike` 📖	CompOp	19 math math: `hasIdealSupport_iff`, `mem_mk`, `isOrdering_iff`, `coe_support`, `pow_two_mem`, `coe_mk'`, `mem_support`, `coe_toSubsemiring`, `mem_of_isSquare`, `mul_self_mem`, `mem_mk'`, `mem_supportAddSubgroup`, `mem_toSubsemiring`, `IsOrdering.toHasMemOrNegMem`, `coe_supportAddSubgroup`, `neg_one_notMem`, `instSubsemiringClass`, `mem_of_isSumSq`, `coe_set_mk`
`support` 📖	CompOp	7 math math: `coe_support`, `instIsPrimeSupport`, `mem_support`, `supportAddSubgroup_eq`, `one_notMem_support`, `IsOrdering.toIsPrime`, `support_eq_bot`
`supportAddSubgroup` 📖	CompOp	5 math math: `supportAddSubgroup_eq`, `mem_supportAddSubgroup`, `one_notMem_supportAddSubgroup`, `coe_supportAddSubgroup`, `supportAddSubgroup_eq_bot`
`toSubsemiring` 📖	CompOp	11 math math: `ext_iff`, `toSubsemiring_strictMono`, `toSubsemiring_lt_toSubsemiring`, `toSubsemiring_mono`, `toSubsemiring_le_toSubsemiring`, `coe_toSubsemiring`, `neg_one_notMem'`, `mem_toSubsemiring`, `mem_of_isSquare'`, `toSubsemiring_inj`, `toSubsemiring_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`SetLike.coe` `RingPreordering` `instSetLike`	`copy`	—	—
`coe_set_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`SetLike.coe` `RingPreordering` `instSetLike` `Subsemiring` `Subsemiring.instSetLike`	—	—
`coe_support` 📖	mathematical	—	`SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `support` `Set` `Set.instInter` `RingPreordering` `instSetLike` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `HasDistribNeg.toInvolutiveNeg` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocRing.toHasDistribNeg`	—	—
`coe_supportAddSubgroup` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddSubgroup.instSetLike` `supportAddSubgroup` `Set` `Set.instInter` `RingPreordering` `instSetLike` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `HasDistribNeg.toInvolutiveNeg` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocRing.toHasDistribNeg`	—	—
`coe_toSubsemiring` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subsemiring.instSetLike` `toSubsemiring` `RingPreordering` `instSetLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `RingPreordering` `instSetLike`	`copy`	—	—
`ext` 📖	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring`	—	—	—
`ext_iff` 📖	mathematical	—	`Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring`	—	`ext`
`hasIdealSupport_iff` 📖	mathematical	—	`HasIdealSupport` `RingPreordering` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`HasIdealSupport.smul_mem_support`
`instHasIdealSupportOfHasMemOrNegMem` 📖	mathematical	—	`HasIdealSupport`	—	`HasMemOrNegMem.mem_or_neg_mem` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass` `mul_neg` `neg_mul` `neg_neg`
`instSubsemiringClass` 📖	mathematical	—	`SubsemiringClass` `RingPreordering` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSetLike`	—	`Subsemiring.mul_mem` `Subsemiring.one_mem` `Subsemiring.add_mem` `Subsemiring.zero_mem`
`mem_copy` 📖	mathematical	`SetLike.coe` `RingPreordering` `instSetLike`	`SetLike.instMembership` `copy` `Set` `Set.instMembership`	—	—
`mem_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`RingPreordering` `SetLike.instMembership` `instSetLike` `Subsemiring` `Subsemiring.instSetLike`	—	—
`mem_of_isSquare` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`RingPreordering` `SetLike.instMembership` `instSetLike`	—	`mem_of_isSquare'`
`mem_of_isSquare'` 📖	mathematical	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring`	—	—
`mem_support` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `support` `RingPreordering` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	—
`mem_supportAddSubgroup` 📖	mathematical	—	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `supportAddSubgroup` `RingPreordering` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`mem_toSubsemiring` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `toSubsemiring` `RingPreordering` `instSetLike`	—	—
`mul_self_mem` 📖	mathematical	—	`RingPreordering` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`mem_of_isSquare`
`neg_one_notMem` 📖	mathematical	—	`RingPreordering` `SetLike.instMembership` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`neg_one_notMem'`
`neg_one_notMem'` 📖	mathematical	—	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`pow_two_mem` 📖	mathematical	—	`RingPreordering` `SetLike.instMembership` `instSetLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`mem_of_isSquare` `IsSquare.sq`
`supportAddSubgroup_eq` 📖	mathematical	—	`supportAddSubgroup` `Submodule.toAddSubgroup` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `support`	—	—
`toSubsemiring_inj` 📖	mathematical	—	`toSubsemiring`	—	`toSubsemiring_injective`
`toSubsemiring_injective` 📖	mathematical	—	`RingPreordering` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toSubsemiring`	—	`ext` `Set.ext`

RingPreordering.HasIdealSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mem_support` 📖	mathematical	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `RingPreordering.supportAddSubgroup`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

RingPreordering.IsOrdering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toHasMemOrNegMem` 📖	mathematical	—	`HasMemOrNegMem` `RingPreordering` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `RingPreordering.instSetLike`	—	—
`toIsPrime` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingPreordering.support` `RingPreordering.instHasIdealSupportOfHasMemOrNegMem` `toHasMemOrNegMem`	—	—

(root)

Definitions

Name	Category	Theorems
`RingPreordering` 📖	CompData	24 math math: `RingPreordering.hasIdealSupport_iff`, `RingPreordering.mem_mk`, `RingPreordering.isOrdering_iff`, `RingPreordering.coe_support`, `RingPreordering.toSubsemiring_strictMono`, `RingPreordering.pow_two_mem`, `RingPreordering.toSubsemiring_lt_toSubsemiring`, `RingPreordering.coe_mk'`, `RingPreordering.toSubsemiring_mono`, `RingPreordering.mem_support`, `RingPreordering.toSubsemiring_le_toSubsemiring`, `RingPreordering.coe_toSubsemiring`, `RingPreordering.mem_of_isSquare`, `RingPreordering.mul_self_mem`, `RingPreordering.mem_mk'`, `RingPreordering.mem_supportAddSubgroup`, `RingPreordering.mem_toSubsemiring`, `RingPreordering.IsOrdering.toHasMemOrNegMem`, `RingPreordering.coe_supportAddSubgroup`, `RingPreordering.neg_one_notMem`, `RingPreordering.instSubsemiringClass`, `RingPreordering.mem_of_isSumSq`, `RingPreordering.toSubsemiring_injective`, `RingPreordering.coe_set_mk`

---

← Back to Index