Theorem LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix

Modification history

2026-06-12 11:46
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: further API for Cartan matrices (#40424)
Added LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrixView on Github →