toLinearMapRight'_mul_apply — Mathlib

English

If M and M' are mutual inverses, the right-equivalence extends to a full linear equivalence on function spaces.

Русский

Если M и M' взаимно обратны, правая эквивалентность расширяется до полной линейной эквивалентности на пространстве функций.

LaTeX

$$toLinearEquivRight'OfInv hMM' hM'M : (n → R) ≃ₗ[R] (m → R)$$

Lean4

theorem toLinearMapRight'_mul_apply [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) (x) :
    Matrix.toLinearMapRight' (M * N) x = Matrix.toLinearMapRight' N (Matrix.toLinearMapRight' M x) :=
  (vecMul_vecMul _ M N).symm

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