diagonal_hadamard_diagonal — Mathlib

English

Let v and w be functions n → α. Then the Hadamard product of the corresponding diagonal matrices equals the diagonal of the pointwise product: diag(v) ⊙ diag(w) = diag(v * w).

Русский

Пусть v и w — функции n → α. Тогда поэлементное произведение соответствующих диагональных матриц равно диагональной матрице, чьи диагональные элементы равны произведению по точкам: diag(v) ⊙ diag(w) = diag(v * w).

LaTeX

$$$\mathrm{diag}(v) \odot \mathrm{diag}(w) = \mathrm{diag}(v * w)$$$

Lean4

theorem diagonal_hadamard_diagonal (v : n → α) (w : n → α) : diagonal v ⊙ diagonal w = diagonal (v * w) :=
  ext fun _ _ => (apply_ite₂ _ _ _ _ _ _).trans (congr_arg _ <| zero_mul 0)

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