English
There is a monoid homomorphism from ring automorphisms to permutations of R, sending each automorphism to its action on the underlying set.
Русский
Существует моноид-гомоморфизм автоморфизмов кольца к перестановкам множества кольца, отправляющий автоморфизм на его действие на множество.
LaTeX
$$$\text{toPerm} : \mathrm{RingAut}(R) \rightarrow^* \mathrm{Equiv.Perm}(R)$ with $\text{toFun} = \mathrm{RingEquiv}.toEquiv$.$$
Lean4
/-- Monoid homomorphism from ring automorphisms to permutations. -/
def toPerm : RingAut R →* Equiv.Perm R where
toFun := RingEquiv.toEquiv
map_one' := rfl
map_mul' _ _ := rfl
