Commit 2025-08-20 21:16 88da4306

View on Github →

chore(LinearAlgebra/Matrix/PosDef): turn IsHermitian.posSemidef_of_eigenvalues_nonneg into an iff (#28576) This turns Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg into an iff, and adds Matrix.IsHermitian.posDef_iff_eigenvalues_pos. Also deletes duplicate proof in PosDef.posSemidef_add and golf.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.IsHermitian.posDef_iff_eigenvalues_pos

added theorem Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg

deleted theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg

deleted theorem Matrix.PosSemidef.eq_sqrt_of_sq_eq