Theorem Matrix.PosDef.toQuadraticForm'

Modification history

2026-06-12 11:46

Mathlib/LinearAlgebra/Matrix/PosDef.lean

feat: further API for Cartan matrices (#40424)

Modified Matrix.PosDef.toQuadraticForm'View on Github →

2023-12-04 20:02

Mathlib/LinearAlgebra/Matrix/PosDef.lean

refactor(LinearAlgebra/Matrix/PosDef): separate `PosDef` lemmas from `PosSemidef` lemmas (#8810) …

Added Matrix.PosDef.toQuadraticForm'View on Github →