Theorem Matrix.PosDef.finite_setOfPred_dotProduct_mulVec_le

Modification history

2026-09-08 16:08
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: supporting API for Cartan matrix realisations (#43460)
Added Matrix.PosDef.finite_setOfPred_dotProduct_mulVec_leView on Github →