mulVecLin — Mathlib

English

mulVecLin is a specialization of vecMulBilin when the ring is commutative, giving a linear map M: (n→R) → (m→R).

Русский

mulVecLin естьSpecialization vecMulBilin в случае коммутативности кольца, задающая линейное отображение.

LaTeX

$$mulVecLin [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R$$

Lean4

/-- `Matrix.mulVec M` as a linear map.

Note this is a special case of `Matrix.mulVecBilin`. -/
abbrev mulVecLin [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R :=
  mulVecBilin R R M

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