diagonal_mul — Mathlib

English

The diagonal multiplication diagonal d on a matrix M gives (diagonal d) * M with entries (i,j) equal to d_i M_{ij}.

Русский

Умножение диагональю diagonal d на матрицу M даёт новые элементы (i,j): d_i M_{ij}.

LaTeX

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

Lean4

@[simp]
theorem diagonal_mul [Fintype m] [DecidableEq m] (d : m → α) (M : Matrix m n α) (i j) :
    (diagonal d * M) i j = d i * M i j :=
  diagonal_dotProduct _ _ _

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