linMulLin_comp — Mathlib

English

For linear maps l, r : M' → M, the bilinear form (linMulLin f g) composed with (l, r) equals linMulLin (f ∘ l) (g ∘ r).

Русский

Для линейных отображений l, r : M' → M равенство билинейной формы (linMulLin f g) скомпозированной с (l, r) и линейной формой linMulLin (f ∘ l) (g ∘ r).

LaTeX

$$$ (\\mathrm{linMulLin}\\; f\\; g) \\circ (l\\, r) = \\mathrm{linMulLin}(f \\circ l) (g \\circ r) $$$

Lean4

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

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