vecMulLinear — Mathlib

English

The operation vecMulVec is a bilinear map in its two vector arguments, producing a rank-one matrix.

Русский

Операция vecMulVec билинейна по двум векторам, порождая матрицу ранга единица.

LaTeX

$$vecMulVecBilin : (m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A$$

Lean4

/-- `Matrix.vecMul M` is a linear map.

Note this is a special case of `Matrix.vecMulBilin`. -/
abbrev vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R :=
  Matrix.vecMulBilin R Rᵐᵒᵖ |>.flip M

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