mul_single_apply_same — Mathlib

English

Right-multiplying a matrix by a single matrix unit concentrates a column: (M * single i j c) has value M(a,i) · c at (a, j).

Русский

Правое умножение матрицы на единичную матрицу концентрирует столбец: (M * single i j c) имеет значение M(a,i) · c в позиции (a, j).

LaTeX

$$$ (M * \mathrm{single}_{i j} c) (a, j) = M(a, i) \cdot c $$$

Lean4

@[simp]
theorem mul_single_apply_same (i : m) (j : n) (a : l) (M : Matrix l m α) : (M * single i j c) a j = M a i * c := by
  simp [mul_apply, single]

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