trans_conj — Mathlib

English

Conjugation by the composition α ≪≫ β equals the composition of the conjugations: (α ≪≫ β).conj f = β.conj (α.conj f).

Русский

Конъюгация конъюгирования по композиции равна композиции конъюгирования: conj(α ≪≫ β) f = β.conj (α.conj f).

LaTeX

$$$\\ (\\alpha \\otimes \\beta).\\mathrm{conj} f = \\beta.\\mathrm{conj}(\\alpha.\\mathrm{conj} f)$$$

Lean4

@[simp]
theorem trans_conj {Z : C} (β : Y ≅ Z) (f : End X) : (α ≪≫ β).conj f = β.conj (α.conj f) :=
  homCongr_trans α α β β f

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