rTensor_comp_apply — Mathlib

English

Right-tensorization preserves multiplication of endomorphisms: (f * g).rTensor M = f.rTensor M * g.rTensor M.

Русский

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

LaTeX

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

Lean4

theorem rTensor_comp_apply (x : N ⊗[R] M) : (g.comp f).rTensor M x = (g.rTensor M) ((f.rTensor M) x) := by
  rw [rTensor_comp, coe_comp]; rfl

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