rTensor_comp — Mathlib

English

Left-tensorization preserves multiplication of endomorphisms: (f * g).lTensor M = f.lTensor M * g.lTensor M.

Русский

Левотензорирование сохраняет умножение эндоморфизмов: (f * g).lTensor M = f.lTensor M * g.lTensor M.

LaTeX

$$$(f * g).lTensor M = f.lTensor M \circ g.lTensor M$$$

Lean4

theorem rTensor_comp : (g.comp f).rTensor M = (g.rTensor M).comp (f.rTensor M) :=
  by
  ext m n
  simp only [compr₂_apply, mk_apply, comp_apply, rTensor_tmul]

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