English
The collection of multiplicative automorphisms of a monoid M forms a group under composition, with multiplication defined by composition, identity the identity automorphism, and inverse the inverse automorphism.
Русский
Множество мультипликативных автоматомов моноида M образует группу под операцией композиции: умножение — композиция, тождественный элемент — тождественный автомат, обратный элемент — обратный автомат.
LaTeX
$$$$ \\text{MulAut}(M) \\text{ is a group under } \\cdot, \\quad g \\cdot h = g \\circ h, \\quad 1 = \\mathrm{id}_M, \\quad g^{-1} = g^{-1}_{\\text{auto}}. $$$$
Lean4
/-- The group operation on multiplicative automorphisms is defined by `g h => MulEquiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
-/
instance : Group (MulAut M) where
mul g h := MulEquiv.trans h g
one := MulEquiv.refl _
inv := MulEquiv.symm
mul_assoc _ _ _ := rfl
one_mul _ := rfl
mul_one _ := rfl
inv_mul_cancel := MulEquiv.self_trans_symm
