English
If e: A ≃* B is a group isomorphism, then for each integer n there is a canonical isomorphism between the quotients A/(z^n) and B/(z^n) induced by e, i.e., an isomorphism that respects z-powers.
Русский
Если e: A ≃* B — изоморфизм групп, то для каждого целого n существует каноническое изоморфизм между квартирами A/(z^n) и B/(z^n), индуцированный e.
LaTeX
$$$\\exists\\, \\text{MulEquiv }\\; e_n: A/(zpowGroupHom n).range \\;\\simeq\\; B/(zpowGroupHom n).range \\quad\\text{induced by } e$$$
Lean4
/-- The equivalence of quotients by powers of an integer induced by a group isomorphism. -/
@[to_additive /-- The equivalence of quotients by multiples of an integer induced by an additive
group isomorphism. -/
]
def equivQuotientZPowOfEquiv : A ⧸ (zpowGroupHom n : A →* A).range ≃* B ⧸ (zpowGroupHom n : B →* B).range :=
MonoidHom.toMulEquiv _ _ (homQuotientZPowOfHom_comp_of_rightInverse (e.symm : B →* A) (e : A →* B) n e.left_inv)
(homQuotientZPowOfHom_comp_of_rightInverse (e : A →* B) (e.symm : B →* A) n e.right_inv)
-- Porting note: had to explicitly coerce the `MulEquiv`s to `MonoidHom`s
