Theorem Matrix.PosDef.of_subsingleton

Modification history

2025-12-09 04:22

Mathlib/LinearAlgebra/Matrix/PosDef.lean

refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)

Added Matrix.PosDef.of_subsingleton View on Github →