single_mul_apply_same — Mathlib

English

Left-multiplying a matrix by a single matrix unit scales a row: (single i j c) * M evaluated at (i, b) equals c · M(j, b).

Русский

Левое умножение единичной матрицы на матрицу масштабирует строку: (single i j c) * M при (i,b) равно c · M(j,b).

LaTeX

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

Lean4

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

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