Canonical

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

Statistics

Metric	Count
Definitions toLinearOrderedCommGroupWithZero	1
Theorems tsub_div	1
Total	2

CanonicallyOrderedAdd

Definitions

Name	Category	Theorems
toLinearOrderedCommGroupWithZero 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tsub_div 📖	mathematical	—	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring	—	div_eq_mul_inv tsub_mul LE.total IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono

---

← Back to Index