Documentation Verification Report

Compare

📁 Source: Mathlib/Tactic/Ring/Compare.lean

Statistics

Metric	Count
Definitions `ExceptType`, `amwo_of_cs`, `evalLE`, `evalLT`, `le_of_po`, `lt_of_po`, `proveLE`, `proveLT`	8
Theorems `add_le_add_left`, `add_le_of_nonpos_left`, `add_lt_add_left`, `add_lt_of_neg_left`, `le_add_of_nonneg_left`, `le_congr`, `lt_add_of_pos_left`, `lt_congr`	8
Total	16

Mathlib.Tactic.Ring

Definitions

Name	Category	Theorems
`ExceptType` 📖	CompData	—
`amwo_of_cs` 📖	CompOp	—
`evalLE` 📖	CompOp	—
`evalLT` 📖	CompOp	—
`le_of_po` 📖	CompOp	—
`lt_of_po` 📖	CompOp	—
`proveLE` 📖	CompOp	—
`proveLT` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_le_add_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`add_le_of_nonpos_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_le_of_nonpos_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`add_lt_add_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`add_lt_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_lt_of_neg_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`le_add_of_nonneg_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`le_congr` 📖	—	—	—	—	—
`lt_add_of_pos_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`lt_congr` 📖	—	—	—	—	—

---

← Back to Index