Commit 2026-06-12 11:46 2ddb51e1

View on Github →

feat: further API for Cartan matrices (#40424)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.isHermitian_iff_isSymm

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix

modified theorem Matrix.PosDef.of_toQuadraticForm'

modified theorem Matrix.PosDef.toQuadraticForm'

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.coe_toWeightBasisInt_apply

added theorem RootPairing.Base.linearIndependentInt

added theorem RootPairing.Base.spanIntRootSupport

added def RootPairing.Base.toWeightBasisInt

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

added theorem RootPairing.Base.cartanMatrix_mul_diagonal_eq

added theorem RootPairing.Base.exists_cartanMatrix_diagaonal_mul_posDef

added theorem RootPairing.Base.exists_cartanMatrix_mul_diagaonal_posDef

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

added theorem RootPairing.rootFormIn_isSymm