conj_apply — Mathlib

English

Conjugation by a linear equivalence yields a linear equivalence between endomorphism spaces.

Русский

Сопряжение линейным эквивалентом переводит эндоморфизмы между пространствами.

LaTeX

$$$e.conj : End_{R'}(M') \to End_{R}(M)$$$

Lean4

theorem conj_apply (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') :
    e.conj f = ((↑e : M₁' →ₛₗ[σ₁'₂'] M₂').comp f).comp (e.symm : M₂' →ₛₗ[σ₂'₁'] M₁') :=
  rfl

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