smul_apply — Mathlib

English

Scalar multiplication distributes entrywise: (r • A)_{ij} = r • (A_{ij}).

Русский

Умножение матрицы на скаляр распределяется по элементам: (r • A)_{ij} = r • (A_{ij}).

LaTeX

$$$ \forall r \in \beta, \ A \in \mathrm{Matrix}\,m\,n\,\alpha, \forall i, j, (r \cdot A)_{ij} = r \cdot (A_{ij})$$$

Lean4

@[simp]
theorem smul_apply [SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n) : (r • A) i j = r • (A i j) :=
  rfl

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