Theorems · Definition · order theory

toIcoDiv

{α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → [hα : Archimedean α] → {p : α} → 0 < p → α → α → ℤ

The unique integer such that this multiple of p, subtracted from b, is in Ico a (a + p).

Defined in

Mathlib.Algebra.Order.ToIntervalMod

Cited by

84 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean