dualMap_apply' — Mathlib

English

For a linear map f: M1 → M2 and a functional g on M2, the action of the dual map is given by f.dualMap g = g ∘ f.

Русский

Для линейного отображения f: M1 → M2 и функционала g на M2, действие дуального отображения задаётся как f.dualMap g = g ∘ f.

LaTeX

$$$$ f^*(g) = g \\circ f \\quad (g \\in \\mathrm{Dual}\\, R\, M_2). $$$$

Lean4

theorem dualMap_apply' (f : M₁ →ₗ[R] M₂) (g : Dual R M₂) : f.dualMap g = g.comp f :=
  rfl

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