diagonal_sub — Mathlib

English

The subtraction of two diagonal matrices is the diagonal of the elementwise difference.

Русский

Разность диагональных матриц равна диагонали по попарному вычитанию элементов.

LaTeX

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

Lean4

@[simp]
theorem diagonal_sub [SubNegZeroMonoid α] (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]

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