compLeft_compRight — Mathlib

English

Let B be a bilinear form on M. For any linear maps l, r : M → M, the bilinear form obtained by applying l to the first argument and then r to the second agrees with the bilinear form obtained by composing B with l on the first argument and r on the second.

Русский

Пусть B — билинейная форма на M. Для любых линейных отображений l, r : M → M тензорная форма, полученная применением l к первому аргументу и затем r ко второму, совпадает с формой B после композиции слева l и справа r.

LaTeX

$$$ (B.compLeft\, l).compRight\, r \;=\; B.\;comp\, l\, r $$$

Lean4

@[simp]
theorem compLeft_compRight (B : BilinForm R M) (l r : M →ₗ[R] M) : (B.compLeft l).compRight r = B.comp l r :=
  rfl

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