linMulLin_compRight — Mathlib

English

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

Русский

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

LaTeX

$$$ (\\mathrm{linMulLin}\\; f\\; g)\\.\\mathrm{compRight}\\; r = \\mathrm{linMulLin} f (g \\circ r) $$$

Lean4

@[simp]
theorem linMulLin_compRight (r : M →ₗ[R] M) : (linMulLin f g).compRight r = linMulLin f (g.comp r) :=
  rfl

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