isDiag_neg_iff — Mathlib

English

For a square matrix A over α with subtraction, A is diagonal if and only if -A is diagonal.

Русский

Для квадратной матрицы A над α с операцией вычитания A диагональна тогда и только тогда, когда -A диагональна.

LaTeX

$$$\\forall {\\alpha} [SubtractionMonoid \\alpha] {A : Matrix \\n n \\ n \\alpha}, (-A).IsDiag \\iff A.IsDiag$$$

Lean4

@[simp]
theorem isDiag_neg_iff [SubtractionMonoid α] {A : Matrix n n α} : (-A).IsDiag ↔ A.IsDiag :=
  ⟨fun ha _ _ h => neg_eq_zero.1 (ha h), IsDiag.neg⟩

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