Theorems · Theorem · order theory

Nat.ceil_lt_mul

∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a b : K},
  1 < b → ↑⌈(b - 1)⁻¹⌉₊ / b < a → ↑⌈a⌉₊ < b * a

Defined in

Mathlib.Algebra.Order.Floor.Semifield

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsOrderedRingFloorSemiring