Commit 2026-01-04 03:21 bdcec9f6

View on Github →

feat(Data/Matrix/Cartan): determinants and simply-laced properties (#33115) This PR adds:

Determinants for G₂ and F₄ Cartan matrices
IsSimplyLaced predicate
Simply-laced theorems for A, D, E families Note: E₆/E₇/E₈ determinants are deferred due to decide recursion limits.

Estimated changes

Modified Mathlib/Data/Matrix/Cartan.lean

added theorem CartanMatrix.F₄_det

added theorem CartanMatrix.G₂_det

added theorem CartanMatrix.isSimplyLaced_A

added theorem CartanMatrix.isSimplyLaced_D

added theorem CartanMatrix.isSimplyLaced_E₆

added theorem CartanMatrix.isSimplyLaced_E₇

added theorem CartanMatrix.isSimplyLaced_E₈

added def Matrix.IsSimplyLaced

added theorem Matrix.isSimplyLaced_transpose