homCongr_eq_arrowCongr — Mathlib

English

Conjugation by i on f equals the corresponding linear conj on f.hom.

Русский

Сопряжение i над f эквивалентно линейному сопряжению над f.hom.

LaTeX

$$$\text{Iso.conj } i f = \langle \text{LinearEquiv.conj } i.toLinearEquiv f.hom \rangle$$$

Lean4

theorem homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) :
    Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr i.toLinearEquiv j.toLinearEquiv f.hom⟩ :=
  rfl

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