toMatrix_smulRight — Mathlib

English

For a linear form f: M1 →ₗ[R] R and a vector x ∈ M2, the matrix of f.smulRight x equals vecMulVec of the representation of x times f composed with the basis map.

Русский

Для линейной формы f: M1 →ₗ[R] R и вектора x ∈ M2 матрица f.smulRight x равна vecMulVec координат x, умноженная на отображение f ∘_basis.

LaTeX

$$$\\text{toMatrix } v_1 v_2 (f.smulRight x) = \\text{vecMulVec} (v_2.repr x) (f \\circ v_1).$$$

Lean4

@[simp]
theorem toMatrix_smulRight (f : M₁ →ₗ[R] R) (x : M₂) :
    toMatrix v₁ v₂ (f.smulRight x) = vecMulVec (v₂.repr x) (f ∘ v₁) :=
  by
  ext i j
  simpa [toMatrix_apply, vecMulVec_apply] using mul_comm _ _

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