Basic

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

Statistics

Metric	Count
Definitions `mk'`	1
Theorems `neg_smul_mem`, `smul_mem`, `mk'`, `coe_mk'`, `eq_zero_of_mem_of_neg_mem`, `hasIdealSupport_of_isUnit_two`, `instHasIdealSupport`, `instHasIdealSupportOfFactIsUnitOfNat`, `instIsPrimeSupport`, `inv_mem`, `isOrdering_iff`, `mem_mk'`, `mem_of_isSumSq`, `one_notMem_support`, `one_notMem_supportAddSubgroup`, `supportAddSubgroup_eq_bot`, `supportAddSubgroup_ne_top`, `support_eq_bot`, `support_ne_top`, `toSubsemiring_le_toSubsemiring`, `toSubsemiring_lt_toSubsemiring`, `toSubsemiring_mono`, `toSubsemiring_strictMono`, `unitsInv_mem`	24
Total	25

RingPreordering

Definitions

Name	Category	Theorems
`mk'` 📖	CompOp	2 math math: `coe_mk'`, `mem_mk'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk'` 📖	mathematical	`Set` `Set.instMembership` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`SetLike.coe` `RingPreordering` `instSetLike` `mk'`	—	—
`eq_zero_of_mem_of_neg_mem` 📖	mathematical	`RingPreordering` `Field.toCommRing` `SetLike.instMembership` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass` `inv_mem` `neg_one_notMem` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one`
`hasIdealSupport_of_isUnit_two` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`HasIdealSupport`	—	`Nat.instAtLeastTwoHAddOfNat` `hasIdealSupport_iff` `IsUnit.exists_right_inv` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `sub_eq_add_neg` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `mul_neg_mem`
`instHasIdealSupport` 📖	mathematical	—	`HasIdealSupport` `Field.toCommRing`	—	`supportAddSubgroup_eq_bot` `IsDomain.to_noZeroDivisors` `instIsDomain`
`instHasIdealSupportOfFactIsUnitOfNat` 📖	mathematical	—	`HasIdealSupport`	—	`Nat.instAtLeastTwoHAddOfNat` `hasIdealSupport_of_isUnit_two` `Fact.out`
`instIsPrimeSupport` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `support` `instHasIdealSupport`	—	`instHasIdealSupport` `support_eq_bot` `Ideal.isPrime_bot` `DivisionRing.toNontrivial` `IsDomain.to_noZeroDivisors` `instIsDomain`
`inv_mem` 📖	mathematical	`RingPreordering` `Field.toCommRing` `SetLike.instMembership` `instSetLike`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass` `one_div` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one`
`isOrdering_iff` 📖	mathematical	—	`IsOrdering` `RingPreordering` `SetLike.instMembership` `instSetLike`	—	`mul_neg` `neg_mul` `neg_neg` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass` `HasMemOrNegMem.neg_mem_of_notMem` `IsOrdering.toHasMemOrNegMem` `instHasIdealSupportOfHasMemOrNegMem` `Ideal.IsPrime.mem_or_mem` `IsOrdering.toIsPrime` `IsOrdering.mk'`
`mem_mk'` 📖	mathematical	`Set` `Set.instMembership` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`RingPreordering` `SetLike.instMembership` `instSetLike` `mk'`	—	—
`mem_of_isSumSq` 📖	mathematical	`IsSumSq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`RingPreordering` `SetLike.instMembership` `instSetLike`	—	`IsSumSq.rec'` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `mem_of_isSquare`
`one_notMem_support` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `support` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`one_notMem_supportAddSubgroup`
`one_notMem_supportAddSubgroup` 📖	mathematical	—	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `supportAddSubgroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`neg_one_notMem`
`supportAddSubgroup_eq_bot` 📖	mathematical	—	`supportAddSubgroup` `Field.toCommRing` `Bot.bot` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddSubgroup.instBot`	—	`AddSubgroup.ext` `eq_zero_of_mem_of_neg_mem` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `instSubsemiringClass` `neg_zero`
`supportAddSubgroup_ne_top` 📖	—	—	—	—	`neg_one_notMem`
`support_eq_bot` 📖	mathematical	—	`support` `Field.toCommRing` `instHasIdealSupport` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`instHasIdealSupport` `supportAddSubgroup_eq_bot`
`support_ne_top` 📖	—	—	—	—	`supportAddSubgroup_ne_top`
`toSubsemiring_le_toSubsemiring` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subsemiring.instPartialOrder` `toSubsemiring` `RingPreordering` `instPartialOrder`	—	—
`toSubsemiring_lt_toSubsemiring` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Subsemiring.instPartialOrder` `toSubsemiring` `RingPreordering` `instPartialOrder`	—	—
`toSubsemiring_mono` 📖	mathematical	—	`Monotone` `RingPreordering` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemiring.instPartialOrder` `toSubsemiring`	—	—
`toSubsemiring_strictMono` 📖	mathematical	—	`StrictMono` `RingPreordering` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemiring.instPartialOrder` `toSubsemiring`	—	—
`unitsInv_mem` 📖	mathematical	`RingPreordering` `SetLike.instMembership` `instSetLike` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Units` `Units.instInv`	—	`MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `instSubsemiringClass` `mem_of_isSquare` `IsSquare.mul_self` `Units.mul_inv_cancel_left`

RingPreordering.HasIdealSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_smul_mem` 📖	mathematical	`RingPreordering` `SetLike.instMembership` `RingPreordering.instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingPreordering.hasIdealSupport_iff`
`smul_mem` 📖	mathematical	`RingPreordering` `SetLike.instMembership` `RingPreordering.instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingPreordering.hasIdealSupport_iff`

RingPreordering.IsOrdering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk'` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingPreordering.support` `RingPreordering.instHasIdealSupportOfHasMemOrNegMem`	`RingPreordering.IsOrdering`	—	`RingPreordering.instHasIdealSupportOfHasMemOrNegMem` `RingPreordering.support_ne_top`

---

← Back to Index