diagonal_add — Mathlib

English

The sum of diagonal matrices is the diagonal matrix of the sum of their defining vectors.

Русский

Сумма диагональных матриц равна диагональной матрице, задаваемой суммой диагоналей.

LaTeX

$$$\\mathrm{diag}(d_1) + \\mathrm{diag}(d_2) = \\mathrm{diag}(d_1 + d_2)$$$

Lean4

@[simp]
theorem diagonal_add [AddZeroClass α] (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]

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