Commit 2026-09-08 16:08 f965aad7

View on Github →

feat: supporting API for Cartan matrix realisations (#43460)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/SerreConstruction.lean

Modified Mathlib/Analysis/Matrix/PosDef.lean

deleted theorem Matrix.PosDef.det_pos

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.col_mul_eq_mulVec_col

added theorem Matrix.row_mul_eq_vecMul_row

Modified Mathlib/GroupTheory/Perm/Fin.lean

Renamed Mathlib/LinearAlgebra/Matrix/Cartan.lean to Mathlib/LinearAlgebra/Matrix/Cartan/Basic.lean

added theorem Matrix.IsFiniteCartan.det_pos

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.IsHermitian.isSymm

added theorem Matrix.IsHermitian.star_dotProduct_mulVec_comm

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.PosDef.det_pos

added theorem Matrix.PosDef.finite_setOfPred_dotProduct_mulVec_le

added theorem Matrix.PosDef.star_dotProduct_mulVec_mul_le

Modified Mathlib/LinearAlgebra/Matrix/Symmetric.lean

added theorem Matrix.IsSymm.dotProduct_mulVec_comm

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

modified def RootPairing.mk'

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coroot'_ne_zero

added theorem RootPairing.root'_ne_zero

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

modified def RootPairing.Equiv.mk'

Modified Mathlib/Logic/Embedding/Basic.lean

Modified MathlibTest/EvalRank.lean