transpose — Mathlib

English

The transpose of a linear map u : M → M' is a linear map Dual R M' → Dual R M defined by (l ↦ l ∘ u).

Русский

Транспозиция линейного отображения u: M → M' задаёт линейное отображение Dual R M' → Dual R M по правилу (l ↦ l ∘ u).

LaTeX

$$$ \\text{transpose} : (M \\to_\\text{lin} M') \\to_\\text{lin} (Dual R M') (Dual R M),\\quad \\text{transpose}(u) = (l \\mapsto l \\circ u) $$$

Lean4

/-- The transposition of linear maps, as a linear map from `M →ₗ[R] M'` to
`Dual R M' →ₗ[R] Dual R M`. -/
def transpose : (M →ₗ[R] M') →ₗ[R] Dual R M' →ₗ[R] Dual R M :=
  (LinearMap.llcomp R M M' R).flip

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