linMulLin_compLeft — Mathlib

English

If l : M → M is a linear map, then the bilinear form (linMulLin f g) composed on the left by l equals linMulLin (f ∘ l) g.

Русский

Пусть l : M → M — линейное отображение. Тогда линейная форма (linMulLin f g), скомпозированная слева с l, равна linMulLin (f ∘ l) g.

LaTeX

$$$ (\\mathrm{linMulLin}\\; f\\; g)\\.\\mathrm{compLeft}\\; l = \\mathrm{linMulLin}(f \\circ l)\\; g $$$

Lean4

@[simp]
theorem linMulLin_compLeft (l : M →ₗ[R] M) : (linMulLin f g).compLeft l = linMulLin (f.comp l) g :=
  rfl

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