Theorems · Definition · order theory

CeilDiv.ceilDiv

{α : Type u_2} →
  {β : Type u_3} →
    {inst : AddCommMonoid α} →
      {inst_1 : PartialOrder α} →
        {inst_2 : AddCommMonoid β} →
          {inst_3 : PartialOrder β} → {inst_4 : SMulZeroClass α β} → [self : CeilDiv α β] → β → α → β

Ceiling division. If a > 0, then b ⌈/⌉ a is the least c such that b ≤ a • c.

Defined in

Mathlib.Algebra.Order.Floor.Div

Cited by

25 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CeilDiv