diagonal_mul_diagonal' — Mathlib

English

Same as above: diag(d1) · diag(d2) = diag(i ↦ d1(i) d2(i)).

Русский

То же самое: diag(d1) · diag(d2) = diag(i ↦ 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

theorem diagonal_mul_diagonal' [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) :
    diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i :=
  diagonal_mul_diagonal _ _

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