mulVec_one — Mathlib

English

For any A, multiplying by the 1×1 identity matrix yields the same result as applying the identity on the right; specifically A · 1 = Aᵀ summed over appropriate index.

Русский

Умножение на единичную матрицу слева возвращает исходный результат; A · 1 = сумма столбцов A^T.

LaTeX

$$$(A) \cdot 1 = \sum_j A^T_j$$

Lean4

theorem mulVec_one [Fintype n] (A : Matrix m n α) : A *ᵥ 1 = ∑ j, Aᵀ j := by ext; simp [mulVec, dotProduct]

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