conj_symm_apply — Mathlib

English

Isomorphic additive groups have isomorphic automorphism groups; a MulEquiv between G and H induces a MulEquiv between AddAut G and AddAut H.

Русский

Изоморфные аддитивные группы имеют изоморфные группы автоморфизмов; MulEquiv между G и H индуцирует MulEquiv между AddAut G и AddAut H.

LaTeX

$${G : Type*, H : Type*} [AddGroup G] [AddGroup H] (φ : G ≃+ H) : MulAut G ≃* MulAut H$$

Lean4

@[simp]
theorem conj_symm_apply [AddGroup G] (g h : G) : (conj g).toMul.symm h = -g + h + g :=
  rfl

Похожие утверждения