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