Commit 2026-01-19 11:57 0c3a7e1f

View on Github →

feat(Data/Matrix/Cartan): add IsSymm lemmas and simplify IsSimplyLaced proofs (#33870) This PR adds symmetry theorems for A, D, and E-series Cartan matrices, and a lemma reducing simply-laced checks to half the entries for symmetric matrices. The E-series and F₄/G₂ proofs are simplified to use decide.

Estimated changes

Modified Mathlib/Data/Matrix/Cartan.lean

added theorem CartanMatrix.A_isSymm

added theorem CartanMatrix.D_isSymm

added theorem CartanMatrix.E₆_isSymm

added theorem CartanMatrix.E₇_isSymm

added theorem CartanMatrix.E₈_isSymm

modified theorem CartanMatrix.isSimplyLaced_E₆

modified theorem CartanMatrix.isSimplyLaced_E₇

modified theorem CartanMatrix.isSimplyLaced_E₈

added theorem Matrix.isSimplyLaced_iff_of_linearOrder