mulVecLin_apply — Mathlib

English

Let R be a commutative semiring. For any matrix M of size m×n over R and any vector v ∶ n → R, the linear map M.mulVecLin applied to v equals the standard matrix–vector product M *ᵥ v.

Русский

Пусть R — коммутативная полускольная арифметика. Для любой матрицы M размером m×n над R и любого вектора v ∶ n → R выполнено: M.mulVecLin v = M *ᵥ v.

LaTeX

$$$\\forall {R} [\\text{CommSemiring } R], \\forall {m n} (M : \\mathrm{Matrix}\\, m\, n\, R) (v : n \\to R),\\; M.mulVecLin\\, v = M \\ast\\!\\vec{v}$$$

Lean4

@[simp]
theorem mulVecLin_apply [Fintype n] (M : Matrix m n R) (v : n → R) : M.mulVecLin v = M *ᵥ v :=
  rfl

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