dualMap_eq_lcomp — Mathlib

English

For a linear map f: M1 → M2, the dual map f^* coincides with left-composition by f, i.e., f^* = (φ ↦ φ ∘ f).

Русский

Для линейного отображения f: M1 → M2 дуальное отображение f^* совпадает с отображением слева по f, то есть f^*(φ) = φ ∘ f.

LaTeX

$$$$ f^* = (\\phi \\mapsto \\phi \\circ f). $$$$

Lean4

theorem dualMap_eq_lcomp (f : M₁ →ₗ[R] M₂) : f.dualMap = f.lcomp R R :=
  rfl

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