vecMulLinear_transpose

Mathlib.LinearAlgebra.Matrix.ToLin

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

English

For a finite index set, Mᵀ.vecMulLinear equals M.mulVecLin.

Русский

Для конечного множителя: M^T.vecMulLinear = M.mulVecLin.

LaTeX

$$$M^\\top.vecMulLinear = M.mulVecLin$$$

Lean4

@[simp]
theorem vecMulLinear_transpose [Fintype n] (M : Matrix m n R) : Mᵀ.vecMulLinear = M.mulVecLin := by ext;
  simp [vecMul_transpose]

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

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

Разделы

Аффилиация

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