inl_conjAct_comm — Mathlib

English

The inclusion and the conjugation action commute: inl (conjAct e n) = e · inl n · e^{-1}.

Русский

Вставка и действие конъюгации коммутируют: inl (conjAct e n) = e · inl n · e^{-1}.

LaTeX

$$$S.inl (S.conjAct e n) = e \\cdot S.inl n \\cdot e^{-1}$$$

Lean4

/-- The inclusion and a conjugation commute. -/
theorem inl_conjAct_comm {e : E} {n : N} : S.inl (S.conjAct e n) = e * S.inl n * e⁻¹ := by
  simp only [conjAct, MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.trans_apply, MonoidHom.apply_ofInjective_symm,
    MulAut.conjNormal_apply, MonoidHom.ofInjective_apply]

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