English
The group operation on automorphisms of a ring is defined by composition: (g h)(x) = g(h(x)).
Русский
Группа автоморфизмов кольца складывается как композиция: (g h)(x) = g(h(x)).
LaTeX
$$$\forall g,h\in \mathrm{RingAut}(R),\ \forall x\in R,\ (g\,h)(x)=g(h(x)).$$$
Lean4
/-- The group operation on automorphisms of a ring is defined by
`fun g h => RingEquiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`. -/
instance : Group (RingAut R) where
mul g h := RingEquiv.trans h g
one := RingEquiv.refl R
inv := RingEquiv.symm
mul_assoc _ _ _ := rfl
one_mul _ := rfl
mul_one _ := rfl
inv_mul_cancel := RingEquiv.self_trans_symm
