Theorems · Inductive type · order theory

CeilDiv

(α : Type u_2) →
  (β : Type u_3) →
    [AddCommMonoid α] →
      [PartialOrder α] → [inst : AddCommMonoid β] → [PartialOrder β] → [SMulZeroClass α β] → Type (max u_2 u_3)

Typeclass for division rounded up. For each a > 0, this asserts the existence of a left adjoint to the map b ↦ a • b : β → β.

Defined in

Mathlib.Algebra.Order.Floor.Div

Cited by

20 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddCommMonoidPartialOrderAddCommMonoidPartialOrderSMulZeroClass