Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `IsOrderedRing`, `IsStrictOrderedRing`	2
Theorems `toCharZero`, `of_mul_nonneg`, `toIsOrderedAddMonoid`, `toIsStrictOrderedRing`, `toMulPosMono`, `toPosMulMono`, `toZeroLEOneClass`, `isDomain`, `noZeroDivisors`, `of_mul_pos`, `toCharZero`, `toIsOrderedCancelAddMonoid`, `toIsOrderedRing`, `toMulPosStrictMono`, `toNoMaxOrder`, `toNontrivial`, `toPosMulStrictMono`, `toZeroLEOneClass`, `instNoMaxOrderOfNontrivial`, `instNoMinOrderOfNontrivial`, `instOrderedRingOfIsStrictOrderedRing`, `one_add_le_one_add_mul_one_sub`, `one_add_le_one_sub_mul_one_add`, `one_sub_le_one_add_mul_one_sub`, `one_sub_le_one_sub_mul_one_add`	25
Total	27

AddMonoidWithOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCharZero` 📖	mathematical	—	`CharZero`	—	`StrictMono.injective` `strictMono_nat_of_lt_succ` `Nat.cast_succ` `lt_add_one`

IsOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_mul_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`IsOrderedRing` `Ring.toSemiring`	—	`mul_sub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_nonneg` `sub_mul`
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`toIsStrictOrderedRing` 📖	mathematical	—	`IsStrictOrderedRing` `Ring.toSemiring`	—	`IsStrictOrderedRing.of_mul_pos` `toIsOrderedAddMonoid` `toZeroLEOneClass` `LE.le.lt_of_ne'` `mul_nonneg` `toPosMulMono` `LT.lt.le` `mul_ne_zero` `LT.lt.ne'`
`toMulPosMono` 📖	mathematical	—	`MulPosMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder`	—	—
`toPosMulMono` 📖	mathematical	—	`PosMulMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder`	—	—
`toZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLE` `PartialOrder.toPreorder`	—	—

IsStrictOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDomain` 📖	mathematical	—	`IsDomain`	—	`Ne.lt_or_gt` `StrictAnti.injective` `strictAnti_mul_left` `toPosMulStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `toIsOrderedRing` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `StrictMono.injective` `strictMono_mul_left_of_pos` `strictAnti_mul_right` `toMulPosStrictMono` `strictMono_mul_right_of_pos` `toNontrivial`
`noZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Ne.lt_or_gt` `LT.lt.ne'` `mul_pos_of_neg_of_neg` `toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `toIsOrderedRing` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `LT.lt.ne` `mul_neg_of_neg_of_pos` `mul_neg_of_pos_of_neg` `toPosMulStrictMono` `mul_pos`
`of_mul_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`IsStrictOrderedRing` `Ring.toSemiring`	—	`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `mul_sub` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_pos` `sub_mul`
`toCharZero` 📖	mathematical	—	`CharZero` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`AddMonoidWithOne.toCharZero` `toZeroLEOneClass` `NeZero.one` `toNontrivial` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `toIsOrderedRing`
`toIsOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`toIsOrderedRing` 📖	mathematical	—	`IsOrderedRing`	—	`IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `toIsOrderedCancelAddMonoid` `toZeroLEOneClass` `PosMulStrictMono.toPosMulMono` `toPosMulStrictMono` `MulPosStrictMono.toMulPosMono` `toMulPosStrictMono`
`toMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder`	—	—
`toNoMaxOrder` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLT` `PartialOrder.toPreorder`	—	`lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `toIsOrderedRing` `one_pos` `toZeroLEOneClass` `NeZero.charZero_one` `toCharZero`
`toNontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`toPosMulStrictMono` 📖	mathematical	—	`PosMulStrictMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder`	—	—
`toZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLE` `PartialOrder.toPreorder`	—	—

(root)

Definitions

Name	Category	Theorems
`IsOrderedRing` 📖	CompData	28 math math: `instIsOrderedRingProd`, `Real.instIsOrderedRing`, `ENNReal.instIsOrderedRing`, `SetSemiring.instIsOrderedRing`, `Subsemiring.toIsOrderedRing`, `Nonneg.isOrderedRing`, `AddOpposite.instIsOrderedRing`, `NatOrdinal.instIsOrderedRing`, `Subring.toIsOrderedRing`, `Filter.Germ.instIsOrderedRing`, `CanonicallyOrderedAdd.toIsOrderedRing`, `SubsemiringClass.toIsOrderedRing`, `IsOrderedRing.mkOfCone`, `IsStrictOrderedRing.toIsOrderedRing`, `Cardinal.isOrderedRing`, `NNReal.instIsOrderedRing`, `FractionalIdeal.instIsOrderedRing`, `MulOpposite.instIsOrderedRing`, `Submodule.instIsOrderedRing`, `WithTop.instIsOrderedRing`, `StarOrderedRing.toIsOrderedRing`, `WithBot.instIsOrderedRing`, `Subalgebra.toIsOrderedRing`, `HahnSeries.instIsOrderedRingLexOfNoZeroDivisors`, `Function.Injective.isOrderedRing`, `AlgebraicGeometry.Scheme.IdealSheafData.instIsOrderedRing`, `IsOrderedRing.of_mul_nonneg`, `ArchimedeanClass.FiniteResidueField.instIsOrderedRing`
`IsStrictOrderedRing` 📖	CompData	25 math math: `ArchimedeanClass.FiniteElement.instIsStrictOrderedRing`, `Nonneg.isStrictOrderedRing`, `Int.instIsStrictOrderedRing`, `HahnSeries.instIsStrictOrderedRingLexOfIsDomain`, `Zsqrtd.instIsStrictOrderedRingCastInt`, `RCLike.toIsStrictOrderedRing`, `Subsemiring.toIsStrictOrderedRing`, `instIsStrictOrderedRingNNRat`, `Num.isStrictOrderedRing`, `Surreal.instIsStrictOrderedRing`, `Subring.toIsStrictOrderedRing`, `Subalgebra.toIsStrictOrderedRing`, `Hyperreal.instIsStrictOrderedRing`, `IsStrictOrderedRing.of_mul_pos`, `Rat.instIsStrictOrderedRing`, `Nat.instIsStrictOrderedRing`, `NNReal.instIsStrictOrderedRing`, `ConditionallyCompleteLinearOrderedField.toIsStrictOrderedRing`, `SubsemiringClass.toIsStrictOrderedRing`, `Function.Injective.isStrictOrderedRing`, `ZNum.isStrictOrderedRing`, `Subfield.toIsStrictOrderedRing`, `Filter.Germ.instIsStrictOrderedRing`, `IsOrderedRing.toIsStrictOrderedRing`, `Real.instIsStrictOrderedRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNoMaxOrderOfNontrivial` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLT` `PartialOrder.toPreorder`	—	`IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `IsOrderedRing.toZeroLEOneClass` `NeZero.one`
`instNoMinOrderOfNontrivial` 📖	mathematical	—	`NoMinOrder` `Preorder.toLT` `PartialOrder.toPreorder`	—	`IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `NeZero.one`
`instOrderedRingOfIsStrictOrderedRing` 📖	mathematical	—	`Semiring.toGrindSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT` `instIsPreorder_mathlib`	—	`instIsPreorder_mathlib` `instOrderedAddOfAddRightMonoOfAddRightReflectLE` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.one` `IsStrictOrderedRing.toNontrivial` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono`
`one_add_le_one_add_mul_one_sub` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`mul_one_sub` `one_add_mul` `Distrib.rightDistribClass` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_assoc` `add_le_add_right`
`one_add_le_one_sub_mul_one_add` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`one_sub_mul` `mul_one_add` `Distrib.leftDistribClass` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_assoc` `add_le_add_right`
`one_sub_le_one_add_mul_one_sub` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mul_one_sub` `one_add_mul` `Distrib.rightDistribClass` `sub_le_sub_iff` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_assoc` `add_comm` `add_le_add_right`
`one_sub_le_one_sub_mul_one_add` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`one_sub_mul` `mul_one_add` `Distrib.leftDistribClass` `sub_le_sub_iff` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `add_assoc` `add_comm` `add_le_add_right`

---

← Back to Index