Theorem Matrix.PosSemidef.det_nonneg

Modification history

2025-11-18 11:33

Mathlib/Analysis/Matrix/PosDef.lean

chore(LinearAlgebra/Matrix): import less analysis (#31518) …

Modified Matrix.PosSemidef.det_nonneg View on Github →

2025-11-11 18:33

Mathlib/Analysis/Matrix/PosDef.lean

chore(LinearAlgebra/Matrix): import less analysis (#31480) …

Modified Matrix.PosSemidef.det_nonneg View on Github →

2025-05-10 11:36

Mathlib/LinearAlgebra/Matrix/PosDef.lean

feat(LinearAlgebra/Matrix/PosDef): Matrix.PosSemidef.det_nonneg (#24725) …

Added Matrix.PosSemidef.det_nonneg View on Github →