English
Monoid homomorphism from ring automorphisms to multiplicative automorphisms exists, sending each automorphism to its multiplicative action.
Русский
Существует моноид-гомоморфизм автоморфизмов кольца в мультипликативные автоморфизмы: автоморфизм отправляется в своё умножение.
LaTeX
$$$\text{toMulAut} : \mathrm{RingAut}(R) \rightarrow^* \mathrm{MulAut}(R) \text{ with } \text{toFun} = \mathrm{RingEquiv}.toMulEquiv.$$$
Lean4
/-- Monoid homomorphism from ring automorphisms to multiplicative automorphisms. -/
def toMulAut : RingAut R →* MulAut R where
toFun := RingEquiv.toMulEquiv
map_one' := rfl
map_mul' _ _ := rfl
