Floor

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

Statistics

Metric	Count
Definitions evalNatCeil, instFloorSemiring	2
Theorems natCeil, natCeil, natCeil, natCeil, ceil_cast, ceil_coe, coe_ceil, coe_floor, floor_cast, floor_coe, floor_def, floor_natCast_div_natCast, intCeil_cast, intFloor_cast	14
Total	16

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalNatCeil 📖	CompOp	—

Mathlib.Meta.NormNum.IsInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCeil 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.ceil Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Int.cast_negOfNat Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing

Mathlib.Meta.NormNum.IsNNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCeil 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Nat.ceil NNRat NNRat.instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat NNRat.instFloorSemiring NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	to_eq NNRat.ceil_cast NNRat.cast_div IsStrictOrderedRing.toCharZero NNRat.cast_natCast

Mathlib.Meta.NormNum.IsNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCeil 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Nat.instAddMonoidWithOne Nat.ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.ceil_natCast

Mathlib.Meta.NormNum.IsRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCeil 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Field.toDivisionRing	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	neg_to_eq Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono

NNRat

Definitions

Name	Category	Theorems
instFloorSemiring 📖	CompOp	8 math math: coe_floor, floor_coe, floor_cast, coe_ceil, ceil_coe, ceil_cast, floor_def, floor_natCast_div_natCast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceil_cast 📖	mathematical	—	Nat.ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder cast DivisionSemiring.toNNRatCast NNRat instSemifield instLinearOrderNNRat instFloorSemiring	—	eq_or_ne cast_zero Nat.ceil_zero instIsStrictOrderedRingNNRat Nat.ceil_eq_iff
ceil_coe 📖	mathematical	—	Nat.ceil Rat.semiring Rat.instPartialOrder FloorRing.toFloorSemiring DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instIsStrictOrderedRing Rat.instFloorRing cast Rat.instNNRatCast NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring	—	Rat.instIsStrictOrderedRing
coe_ceil 📖	mathematical	—	Nat.ceil NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring Int.ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing cast Rat.instNNRatCast	—	Int.natCast_ceil_eq_ceil Rat.instIsStrictOrderedRing coe_nonneg
coe_floor 📖	mathematical	—	Nat.floor NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring Int.floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing cast Rat.instNNRatCast	—	Int.natCast_floor_eq_floor Rat.instIsStrictOrderedRing coe_nonneg
floor_cast 📖	mathematical	—	Nat.floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder cast DivisionSemiring.toNNRatCast NNRat instSemifield instLinearOrderNNRat instFloorSemiring	—	Nat.floor_eq_iff cast_nonneg Nat.cast_one instIsStrictOrderedRingNNRat
floor_coe 📖	mathematical	—	Nat.floor Rat.semiring Rat.instPartialOrder FloorRing.toFloorSemiring DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instIsStrictOrderedRing Rat.instFloorRing cast Rat.instNNRatCast NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring	—	Rat.instIsStrictOrderedRing
floor_def 📖	mathematical	—	Nat.floor NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring num den	—	coe_floor Rat.floor_def' den_coe num_coe
floor_natCast_div_natCast 📖	mathematical	—	Nat.floor NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instFloorSemiring instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Rat.natFloor_natCast_div_natCast
intCeil_cast 📖	mathematical	—	Int.ceil DivisionRing.toRing Field.toDivisionRing cast DivisionRing.toNNRatCast Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing Rat.instNNRatCast	—	Int.ceil_eq_iff coe_ceil sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing cast_strictMono Nat.ceil_lt_add_one instIsStrictOrderedRingNNRat zero_le instCanonicallyOrderedAdd Eq.trans_lt Int.cast_natCast cast_natCast cast_one cast_add IsStrictOrderedRing.toCharZero cast_le_natCast Nat.le_ceil
intFloor_cast 📖	mathematical	—	Int.floor DivisionRing.toRing Field.toDivisionRing cast DivisionRing.toNNRatCast Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing Rat.instNNRatCast	—	Int.floor_eq_iff coe_floor Nat.cast_one Int.cast_one Int.cast_natCast Nat.cast_add_one Nat.floor_eq_iff zero_le instCanonicallyOrderedAdd

---

← Back to Index