PUnit

📁 Source: Mathlib/Algebra/Order/PUnit.lean

Statistics

Metric	Count
Definitions instLinearOrderedAddCommMonoidWithTop	1
Theorems canonicallyOrderedAdd, isOrderedCancelAddMonoid	2
Total	3

PUnit

Definitions

Name	Category	Theorems
instLinearOrderedAddCommMonoidWithTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd instAdd_mathlib Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	—
isOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid AddCommGroup.toAddCommMonoid addCommGroup SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	le_refl

---

← Back to Index