English
Isomorphic additive groups yield compatible congruences between their automorphism structures; a AddEquiv induces Additions to MulAut.
Русский
Изоморфные аддитивные группы дают согласованные конгруэнции между их структурами автоморфизмов; AddEquiv индуцирует AddAut.
LaTeX
$${G : Type*} [AddGroup G] {H : Type*} [AddGroup H] (φ : AddEquiv G H) (x : AddAut G) → ...$$
Lean4
/-- Isomorphic additive groups have isomorphic automorphism groups. -/
@[simps]
def congr [AddGroup G] {H : Type*} [AddGroup H] (ϕ : G ≃+ H) : AddAut G ≃* AddAut 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]
