English
There is a natural equivalence between the quotient α / zmultiples p and the interval (a, a+p] in α, respecting order and additive structure.
Русский
Существует естественное эквивалентное отображение между фактор-группой α / zmultiples p и интервалом (a, a+p], сохраняющее порядок и сложение.
LaTeX
$$$$ \alpha / \langle p \rangle \;\cong\; (a, a+p] $$$$
Lean4
/-- `toIocMod` as an equiv from the quotient. -/
@[simps symm_apply]
def equivIocMod (a : α) : α ⧸ AddSubgroup.zmultiples p ≃ Set.Ioc a (a + p)
where
toFun b := ⟨(toIocMod_periodic hp a).lift b, QuotientAddGroup.induction_on b <| toIocMod_mem_Ioc hp a⟩
invFun := (↑)
right_inv b := Subtype.ext <| (toIocMod_eq_self hp).mpr b.prop
left_inv
b := by
induction b using QuotientAddGroup.induction_on
dsimp
rw [QuotientAddGroup.eq_iff_sub_mem, toIocMod_sub_self]
apply AddSubgroup.zsmul_mem_zmultiples
