transpose_apply

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Module.Dual.transpose_apply

English

For any u and l, transpose u applied to l equals l composed with u; i.e., transpose u l = l ∘ u.

Русский

Для любого u и l: transpose u l = l ∘ u.

LaTeX

$$$ \\mathrm{transpose}\\; u\\; l = l \\circ u $$$

Lean4

theorem transpose_apply (u : M →ₗ[R] M') (l : Dual R M') : transpose u l = l.comp u :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru