English
Isomorphic additive groups have isomorphic automorphism groups; in particular, a MulEquiv between G and H induces a MulEquiv between AddAut G and AddAut H.
Русский
Изоморфные дополнительных группы имеют изоморфные группы автоморфизмов; например, MulEquiv между G и H порождает MulEquiv между AddAut G и AddAut H.
LaTeX
$$$[Group\ G] [Group\ H] (\phi : G \simeq_* H) : MulAut G \simeq_* MulAut H$$
Lean4
/-- Isomorphic groups have isomorphic automorphism groups. -/
@[simps]
def congr [Group G] {H : Type*} [Group H] (ϕ : G ≃* H) : MulAut G ≃* MulAut H
where
toFun f := ϕ.symm.trans (f.trans ϕ)
invFun f := ϕ.trans (f.trans ϕ.symm)
left_inv _ := by simp [DFunLike.ext_iff]
right_inv _ := by simp [DFunLike.ext_iff]
map_mul' := by simp [DFunLike.ext_iff]
