toPerm — Mathlib

English

There is a natural monoid hom from AddAut A to Equiv.Perm A sending each automorphism to its underlying permutation.

Русский

Существует естественный моноид-гомоморфизм от AddAut A к Equiv.Perm A, отправляющий автоморфизм в соответствующую перестановку.

LaTeX

$$$\mathrm{toPerm}: \mathrm{AddAut}(A) \to_* \mathrm{Equiv.Perm}(A)$ with \; \mathrm{toPerm}(e) = \mathrm{AddEquiv}.toEquiv(e)$$$

Lean4

/-- Monoid hom from the group of multiplicative automorphisms to the group of permutations. -/
def toPerm : AddAut A →* Equiv.Perm A where
  toFun := AddEquiv.toEquiv
  map_one' := rfl
  map_mul' _ _ := rfl

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