Theorems · Definition · order theory

toIcoMod

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

Reduce b to the interval Ico a (a + p).

Defined in

Mathlib.Algebra.Order.ToIntervalMod

Cited by

99 results in Mathlib

Foundations

Depth 53 from the axioms, rests on 1,019 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean