toLinearMapRight'_mul — Mathlib

English

Applying the right map to a product M N equals the composition of right maps for N and M.

Русский

Применение правой карты к произведению M N равно композиции правых карт N и M.

LaTeX

$$Matrix.toLinearMapRight'(M N) = (Matrix.toLinearMapRight' N).comp (Matrix.toLinearMapRight' M)$$

Lean4

@[simp]
theorem toLinearMapRight'_mul [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) :
    Matrix.toLinearMapRight' (M * N) = (Matrix.toLinearMapRight' N).comp (Matrix.toLinearMapRight' M) :=
  LinearMap.ext fun _x ↦ (vecMul_vecMul _ M N).symm

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