trace_eq_zero_iff — Mathlib

English

For PSD A, trace zero implies A = 0 and conversely.

Русский

Для PSD A trace(A) = 0 эквивалентно A = 0.

LaTeX

$$PosSemidef(A) → (trace(A) = 0 ⇔ A = 0)$$

Lean4

theorem trace_eq_zero_iff {A : Matrix n n 𝕜} (hA : A.PosSemidef) : A.trace = 0 ↔ A = 0 :=
  by
  refine ⟨fun h => ?_, fun h => h ▸ trace_zero n 𝕜⟩
  classical
  simp_rw [hA.isHermitian.trace_eq_sum_eigenvalues, ← RCLike.ofReal_sum, RCLike.ofReal_eq_zero,
    Finset.sum_eq_zero_iff_of_nonneg (s := Finset.univ) (by simpa using hA.eigenvalues_nonneg), Finset.mem_univ,
    true_imp_iff] at h
  exact funext_iff.eq ▸ hA.isHermitian.eigenvalues_eq_zero_iff.mp <| h

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