Documentation Verification Report

Ring

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

Statistics

Metric	Count
Definitions `addCommSemigroup`, `addLeftCancelSemigroup`, `addRightCancelSemigroup`, `addSemigroup`, `commMonoid`, `instAddSubtypeLtOfNat_mathlib`, `instDistribSubtypeLtOfNat`, `instMonoidSubtypeLtOfNat`, `instMulSubtypeLtOfNat_mathlib`, `instOneSubtypeLtOfNat_mathlib`, `instPowSubtypeLtOfNatNat_mathlib`, `instSemigroupSubtypeLtOfNat`	12
Theorems `addLeftMono`, `addLeftReflectLE`, `addLeftReflectLT`, `addLeftStrictMono`, `addRightReflectLE`, `addRightReflectLT`, `addRightStrictMono`, `coe_add`, `isOrderedCancelMonoid`, `isOrderedMonoid`, `val_mul`, `val_one`, `val_pow`	13
Total	25

Positive

Definitions

Name	Category	Theorems
`addCommSemigroup` 📖	CompOp	—
`addLeftCancelSemigroup` 📖	CompOp	—
`addRightCancelSemigroup` 📖	CompOp	—
`addSemigroup` 📖	CompOp	—
`commMonoid` 📖	CompOp	2 math math: `isOrderedMonoid`, `isOrderedCancelMonoid`
`instAddSubtypeLtOfNat_mathlib` 📖	CompOp	8 math math: `addRightReflectLE`, `addLeftStrictMono`, `addLeftReflectLE`, `addLeftMono`, `addRightReflectLT`, `addLeftReflectLT`, `addRightStrictMono`, `coe_add`
`instDistribSubtypeLtOfNat` 📖	CompOp	—
`instMonoidSubtypeLtOfNat` 📖	CompOp	7 math math: `UpperHalfPlane.coe_pos_real_smul`, `UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero`, `UpperHalfPlane.pos_real_smul_injective`, `UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero`, `UpperHalfPlane.pos_real_re`, `UpperHalfPlane.pos_real_im`, `UpperHalfPlane.isometry_pos_mul`
`instMulSubtypeLtOfNat_mathlib` 📖	CompOp	4 math math: `Nonneg.val_unitsEquivPos_symm_apply_coe`, `val_mul`, `Nonneg.unitsEquivPos_apply_coe`, `Nonneg.val_inv_unitsEquivPos_symm_apply_coe`
`instOneSubtypeLtOfNat_mathlib` 📖	CompOp	1 math math: `val_one`
`instPowSubtypeLtOfNatNat_mathlib` 📖	CompOp	1 math math: `val_pow`
`instSemigroupSubtypeLtOfNat` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib` `Preorder.toLE`	—	`StrictMono.monotone` `add_lt_add_right` `addLeftStrictMono`
`addLeftReflectLE` 📖	mathematical	—	`AddLeftReflectLE` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib` `Preorder.toLE`	—	`Subtype.coe_le_coe` `le_of_add_le_add_left`
`addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLT` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib`	—	`Subtype.coe_lt_coe` `lt_of_add_lt_add_left`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib`	—	`Subtype.coe_lt_coe` `add_lt_add_right`
`addRightReflectLE` 📖	mathematical	—	`AddRightReflectLE` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib` `Preorder.toLE`	—	`Subtype.coe_le_coe` `le_of_add_le_add_right`
`addRightReflectLT` 📖	mathematical	—	`AddRightReflectLT` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib`	—	`Subtype.coe_lt_coe` `lt_of_add_lt_add_right`
`addRightStrictMono` 📖	mathematical	—	`AddRightStrictMono` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib`	—	`Subtype.coe_lt_coe` `add_lt_add_left`
`coe_add` 📖	mathematical	—	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddSubtypeLtOfNat_mathlib` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`isOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commMonoid` `Subtype.partialOrder`	—	`isOrderedMonoid` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`isOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commMonoid` `Subtype.partialOrder`	—	`Subtype.coe_le_coe` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `LT.lt.le`
`val_mul` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMulSubtypeLtOfNat_mathlib` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`val_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instOneSubtypeLtOfNat_mathlib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`val_pow` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instPowSubtypeLtOfNatNat_mathlib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—

---

← Back to Index