Floor

📁 Source: Mathlib/Algebra/Order/Nonneg/Floor.lean

Statistics

Metric	Count
Definitions floorSemiring	1
Theorems nat_ceil_coe, nat_floor_coe	2
Total	3

Nonneg

Definitions

Name	Category	Theorems
floorSemiring 📖	CompOp	2 math math: nat_ceil_coe, nat_floor_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_ceil_coe 📖	mathematical	—	Nat.ceil Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring IsOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Subtype.partialOrder floorSemiring	—	—
nat_floor_coe 📖	mathematical	—	Nat.floor Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring IsOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Subtype.partialOrder floorSemiring	—	—

---

← Back to Index