English
There exists a natural equivalence between the quotient of α by the zmultiples of p and the half-open interval [a, a+p) in α, compatible with the group structure and order.
Русский
Существует естественное эквивалентное отображение между фактор-группой α по zmultiples p и полузакрытым интервалом [a, a+p) в α, сохраняющее структуру группы и порядок.
LaTeX
$$$$ \alpha / \langle p \rangle \;\cong\; [a, a+p) \quad\text{(as a suitable equivalence of structures)} $$$$
Lean4
/-- `toIcoMod` as an equiv from the quotient. -/
@[simps symm_apply]
def equivIcoMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ico a (a + p)
where
toFun b := ⟨(toIcoMod_periodic hp a).lift b, QuotientAddGroup.induction_on b <| toIcoMod_mem_Ico hp a⟩
invFun := (↑)
right_inv b := Subtype.ext <| (toIcoMod_eq_self hp).mpr b.prop
left_inv
b := by
induction b using QuotientAddGroup.induction_on
dsimp
rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]
apply AddSubgroup.zsmul_mem_zmultiples
