Mathlib Map

Theorems · Theorem · number theory

NNRat.ceil_cast

∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (x : ℚ≥0), ⌈↑x⌉₊ = ⌈x⌉₊
Defined in
Mathlib.Data.NNRat.Floor
Cited by
1 results in Mathlib
Foundations
Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SemifieldLinearOrderIsStrictOrderedRingFloorSemiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib.Meta.NormNum.IsNNRat.natCeil · cited by 0IsNNRat.natCeilLinearOrder · cited by 8572LinearOrderIsStrictOrderedRing · cited by 2490IsStrictOrderedRingeq_or_ne · cited by 1117eq_or_neNNRat · cited by 523NNRatSemifield · cited by 439SemifieldNNRat.cast · cited by 235NNRat.castFloorSemiring · cited by 179FloorSemiringNat.ceil · cited by 141Nat.ceilNNRat.cast_zero · cited by 6NNRat.cast_zeroNat.ceil_eq_iff · cited by 3Nat.ceil_eq_iffNat.ceil_zero · cited by 3Nat.ceil_zeroNNRat.ceil_castCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.