smul_single — Mathlib

English

Scaling a single matrix by r distributes to the single with scaled entry.

Русский

Умножение на скаляр в единственной матрице распределяется на изменённый элемент.

LaTeX

$$$r \cdot (\text{single } i j a) = \text{single } i j (r \cdot a).$$$

Lean4

@[simp]
theorem smul_single [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) : r • single i j a = single i j (r • a) :=
  by
  unfold single
  ext
  simp [smul_ite]

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