diagonal_eq_diagonal_iff — Mathlib

English

Two diagonals are equal iff their diagonal entries agree pointwise.

Русский

Два диагональных равно diag(d1) и diag(d2) равны тогда и только тогда, когда их диагональные элементы совпадают по каждому индексу.

LaTeX

$$$diag(d_1) = diag(d_2) \\iff \\forall i, d_1(i) = d_2(i)$$$

Lean4

@[simp]
theorem diagonal_eq_diagonal_iff [Zero α] {d₁ d₂ : n → α} : diagonal d₁ = diagonal d₂ ↔ ∀ i, d₁ i = d₂ i :=
  ⟨fun h i => by simpa using congr_arg (fun m : Matrix n n α => m i i) h, fun h => by rw [show d₁ = d₂ from funext h]⟩

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