English
There is a natural monoid homomorphism from MulAut M to the permutation group of M, which sends each automorphism to its underlying permutation of M.
Русский
Существует естественный гомоморфизм моноида от MulAut M к группе перестановок M, который присваивает каждому автоморфизм его подлежащую перестановку M.
LaTeX
$$$\mathrm{toPerm}: \mathrm{MulAut}(M) \to_* \mathrm{Equiv.Perm}(M)$ with \; \mathrm{toPerm}(e) = \mathrm{MulEquiv}.toEquiv(e)$$$
Lean4
/-- Monoid hom from the group of multiplicative automorphisms to the group of permutations. -/
def toPerm : MulAut M →* Equiv.Perm M where
toFun := MulEquiv.toEquiv
map_one' := rfl
map_mul' _ _ := rfl
