mulVecLin_transpose

Mathlib.LinearAlgebra.Matrix.ToLin

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

English

For a finite index set of size m, the transpose of a matrix M yields that Mᵀ.mulVecLin equals M.vecMulLinear.

Русский

Для конечного множителя размера m верно: Mᵀ.mulVecLin = M.vecMulLinear.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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