rTensor_comp_lTensor — 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

@[simp]
theorem rTensor_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (f.rTensor Q).comp (g.lTensor M) = map f g := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

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