conj_comp — Mathlib

English

Conjugation by an isomorphism α is compatible with composition: α.conj(f ∘ g) = α.conj(f) ∘ α.conj(g).

Русский

Умножение через конъюгацию взглядом изоморфизма α совместимо с композицией: α.conj(f ∘ g) = α.conj(f) ∘ α.conj(g).

LaTeX

$$$\\alpha.\\mathrm{conj}(f \\circ g) = \\alpha.\\mathrm{conj}(f) \\circ \\alpha.\\mathrm{conj}(g)$$$

Lean4

@[simp]
theorem conj_comp (f g : End X) : α.conj (f ≫ g) = α.conj f ≫ α.conj g :=
  map_mul α.conj g f

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