mulEquivPerm — Mathlib

English

There is a canonical group isomorphism Aut(α) ≅ Sym(α) between the automorphism group of a type α and the permutation group on α.

Русский

Существует каноническое изоморфизм между группой автоморфизмов Aut(α) и группой перестановок Sym(α).

LaTeX

$$$\mathrm{Aut}(\alpha) \cong \mathrm{Sym}(\alpha)$$$

Lean4

/-- The (unbundled) group of automorphisms of a type is `MulEquiv` to the (unbundled) group
of permutations. -/
def mulEquivPerm {α : Type u} : Aut α ≃* Equiv.Perm α :=
  isoPerm.groupIsoToMulEquiv

Похожие утверждения