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)