English
Isomorphisms between groups induce corresponding isomorphisms between their automorphism groups with compatible inverses.
Русский
Изоморфизмы между группами порождают соответствующие изоморфизмы между их группами автоморфизмов с совместимыми обратными.
LaTeX
$$$[Group\ G] {H} [Group H] (\phi : G \simeq_* H) (x : MulAut G) -> ...$$$
Lean4
/-- The group operation on additive automorphisms is defined by `g h => AddEquiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
-/
instance group : Group (AddAut A) where
mul g h := AddEquiv.trans h g
one := AddEquiv.refl _
inv := AddEquiv.symm
mul_assoc _ _ _ := rfl
one_mul _ := rfl
mul_one _ := rfl
inv_mul_cancel := AddEquiv.self_trans_symm
