English
The group isomorphism between alternating groups is induced by a given equivalence e: α ≃ β.
Русский
Групповой изоморфизм между чередующими группами индуцируется данным эквивалентным отображением e: α ≃ β.
LaTeX
$$$\text{altCongrHom}_{\alpha,\beta}(e) : \mathrm{Alt}(\alpha) \cong \mathrm{Alt}(\beta)$ for every bijection e : \alpha \simeq \beta$$$
Lean4
/-- The group isomorphism between `alternatingGroup`s induced by the given `Equiv`. -/
@[simps ! apply_coe]
def altCongrHom {β : Type*} [Fintype β] [DecidableEq β] (e : α ≃ β) : ↥(alternatingGroup α) ≃* ↥(alternatingGroup β) :=
e.permCongrHom.subgroupMap (alternatingGroup α) |>.trans <|
MulEquiv.subgroupCongr <| by simp [Subgroup.ext_iff, Subgroup.map_equiv_eq_comap_symm]
