one_vecMul

Mathlib.Data.Matrix.Mul

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

English

The product of the all-ones column with a matrix equals the sum of the columns of the matrix.

Русский

Произведение столбца единиц на матрицу даёт сумму столбцов матрицы.

LaTeX

$$1^T · A = ∑_i A_i$$

Lean4

theorem one_vecMul [Fintype m] (A : Matrix m n α) : 1 ᵥ* A = ∑ i, A i := by ext; simp [vecMul, dotProduct]

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

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

Разделы

Аффилиация

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