linMulLin_comp — Mathlib

English

linMulLin respects precomposition: (linMulLin f g).comp h = linMulLin (f.comp h) (g.comp h).

Русский

LinMulLin сохраняет композицию слева: линMulLin f g после предсоставления через h эквивалентно линMulLin (f∘h) (g∘h).

LaTeX

$$$(\operatorname{linMulLin} f g) \circ h = \operatorname{linMulLin}(f\circ h)(g\circ h).$$$

Lean4

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

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