coe_mulVecLin

Mathlib.LinearAlgebra.Matrix.ToLin

URI: https://scilib.ai/kg/mathlib#Matrix.coe_mulVecLin

English

The coercion of mulVecLin equals the standard mulVec on matrices.

Русский

Приведение mulVecLin к функции совпадает с обычным mulVec.

LaTeX

$$coe_mulVecLin [Fintype n] (M : Matrix m n R) : (M.mulVecLin : _ → _) = M.mulVec$$

Lean4

theorem coe_mulVecLin [Fintype n] (M : Matrix m n R) : (M.mulVecLin : _ → _) = M.mulVec :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru