zero_mul — Mathlib

English

Multiplication by a diagonal matrix diag(d) scales each row i of a matrix M by d_i: (diag(d) * M)_{i j} = d_i M_{i j}.

Русский

Умножение диагональной матрицы diag(d) на M масштабирует i-ую строку на d_i: (diag(d) M)_{ij} = d_i M_{ij}.

LaTeX

$$$ (\text{diag}(d) * M)_{ij} = d_i M_{ij} $$$

Lean4

@[simp]
protected theorem zero_mul [Fintype m] (M : Matrix m n α) : (0 : Matrix l m α) * M = 0 :=
  by
  ext
  apply zero_dotProduct

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