English
If d1 and d2 are functions from a finite set n to α, then the product of the corresponding diagonal matrices is the diagonal matrix with entries d1(i) d2(i) on the i-th diagonal position: diag(d1) · diag(d2) = diag(i ↦ d1(i) d2(i)).
Русский
Если d1 и d2 — функции из конечного множества n в α, то произведение диагональных матриц diag(d1) и diag(d2) равно диагональной diag(d1(i) d2(i)).
LaTeX
$$$\\operatorname{diagonal}(d_1) \\cdot \\operatorname{diagonal}(d_2) = \\operatorname{diagonal}(i \\mapsto d_1(i) \\cdot d_2(i))$$$
Lean4
@[simp]
theorem diagonal_mul_diagonal [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) :
diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i :=
by
ext i j
by_cases h : i = j <;> simp [h]
