transpose_comp — Mathlib

English

Let M, M′, M″ be modules over a commutative semiring R, and let u: M′ → M″ and v: M → M′ be linear maps. Then the transpose respects composition in the reverse order: transpose(u ∘ v) = (transpose v) ∘ (transpose u).

Русский

Пусть M, M′, M″ — модули над коммутативным полем R, и u: M′ → M″, v: M → M′ — линейные отображения. Тогда транспонирование сохраняет композицию в обратном порядке: transpose(u ∘ v) = (transpose v) ∘ (transpose u).

LaTeX

$$$$ \\operatorname{transpose}(u \\circ v) = (\\operatorname{transpose} v) \\circ (\\operatorname{transpose} u). $$$$

Lean4

theorem transpose_comp (u : M' →ₗ[R] M'') (v : M →ₗ[R] M') : transpose (u.comp v) = (transpose v).comp (transpose u) :=
  rfl

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