Order

📁 Source: Mathlib/Data/NNRat/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems instCanonicallyOrderedAdd, instOrderedSub, instIsStrictOrderedRingNNRat	3
Total	3

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringNNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat	—	Nonneg.canonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing
instOrderedSub 📖	mathematical	—	OrderedSub NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringNNRat instSubNNRat	—	Nonneg.orderedSub Rat.instIsStrictOrderedRing

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStrictOrderedRingNNRat 📖	mathematical	—	IsStrictOrderedRing NNRat CommSemiring.toSemiring instCommSemiringNNRat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat	—	Nonneg.isStrictOrderedRing Rat.instIsStrictOrderedRing

---

← Back to Index