Theorems · Theorem · order theory

Int.ceil_lt_mul

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

Defined in

Mathlib.Algebra.Order.Floor.Ring

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsOrderedRingFloorRing