conj_hom_eq_conj — Mathlib

English

For V ≅ W and f ∈ End(V), the hom-component of the conjugation corresponds to the linear conjugation of f.hom by isoToLinearEquiv(i).

Русский

Для V ≅ W и f ∈ End(V), компоненту по гомоморфизму коньюгации соответствует действие линейного коньюгирования f.hom через isoToLinearEquiv(i).

LaTeX

$$$ (Iso.conj i f).hom = LinearEquiv.conj( isoToLinearEquiv(i) ) (f.hom). $$$

Lean4

theorem conj_hom_eq_conj {V W : FGModuleCat R} (i : V ≅ W) (f : End V) :
    (Iso.conj i f).hom = (LinearEquiv.conj (isoToLinearEquiv i) f.hom) :=
  rfl

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