Theorems · Definition · order theory

QuotientAddGroup.equivIocMod

{α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → 0 < p → (a : α) → α ⧸ AddSubgroup.zmultiples p ≃ ↑(Set.Ioc a (a + p))

toIocMod as an equiv from the quotient.

Defined in

Mathlib.Algebra.Order.ToIntervalMod

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean