Documentation Verification Report

Canonical

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

Statistics

Metric	Count
Definitions	0
Theorems `mul_tsub`, `tsub_mul`, `mul_lt_mul_of_lt_of_lt`, `mul_pos`, `pow_pos`, `toIsOrderedMonoid`, `toIsOrderedRing`, `toMulLeftMono`, `toMulRightMono`, `toZeroLEOneClass`, `pos`, `mul_self_tsub_mul_self`, `mul_self_tsub_one`, `mul_tsub`, `mul_tsub_one`, `sq_tsub_sq`, `tsub_mul`, `tsub_one_mul`	18
Total	18

AddLECancellable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_tsub` 📖	—	`AddLECancellable` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul`	—	—	`total_of` `tsub_eq_zero_iff_le` `MulZeroClass.mul_zero` `mul_le_mul_right` `CanonicallyOrderedAdd.toMulLeftMono` `eq_tsub_of_add_eq` `mul_add` `Distrib.leftDistribClass` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`
`tsub_mul` 📖	—	`AddLECancellable` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul`	—	—	`total_of` `tsub_eq_zero_iff_le` `MulZeroClass.zero_mul` `mul_le_mul_left` `eq_tsub_of_add_eq` `add_mul` `Distrib.rightDistribClass` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`

CanonicallyOrderedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_lt_mul_of_lt_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`posMulStrictMono_iff_mulPosStrictMono` `CommMagma.to_isCommutative` `eq_zero_or_pos` `MulZeroClass.mul_zero` `mul_pos` `LE.le.trans_lt` `zero_le` `mul_lt_mul_of_pos'`
`mul_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`pow_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pos_iff_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `LT.lt.ne'`
`toIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `CommSemiring.toCommMonoid`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `toMulLeftMono`
`toIsOrderedRing` 📖	mathematical	—	`IsOrderedRing` `CommSemiring.toSemiring`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `toAddLeftMono` `toZeroLEOneClass` `MulLeftMono.toPosMulMono` `toMulLeftMono` `MulRightMono.toMulPosMono` `covariant_swap_mul_of_covariant_mul`
`toMulLeftMono` 📖	mathematical	—	`MulLeftMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ExistsAddOfLE.exists_add_of_le` `toExistsAddOfLE` `mul_add` `Distrib.leftDistribClass` `self_le_add_right`
`toMulRightMono` 📖	mathematical	—	`MulRightMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ExistsAddOfLE.exists_add_of_le` `toExistsAddOfLE` `add_mul` `Distrib.rightDistribClass` `self_le_add_right`
`toZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`zero_le`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pos` 📖	mathematical	`Odd`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`CanonicallyOrderedAdd.toZeroLEOneClass` `NeZero.one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_self_tsub_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toAdd`	—	`mul_tsub` `add_mul` `Distrib.rightDistribClass` `tsub_add_eq_tsub_tsub` `mul_comm` `add_tsub_cancel_right`
`mul_self_tsub_one` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd`	—	`mul_self_tsub_mul_self` `mul_one`
`mul_tsub` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddLECancellable.mul_tsub` `Contravariant.AddLECancellable`
`mul_tsub_one` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_tsub` `mul_one`
`sq_tsub_sq` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd`	—	`sq` `mul_self_tsub_mul_self`
`tsub_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddLECancellable.tsub_mul` `Contravariant.AddLECancellable`
`tsub_one_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`tsub_mul` `one_mul`

---

← Back to Index