∀ {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (d₁ d₂ : n → α), Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i * d₂ i