Commit 2025-12-19 18:36 aa462dbf

View on Github →

feat(Data/Matrix/Cartan): off-diagonal and transpose for exceptional matrices (#32998) Adds off-diagonal bounds and transpose properties for exceptional Cartan matrices, completing the property coverage begun in #32967

Estimated changes

Modified Mathlib/Data/Matrix/Cartan.lean

added theorem CartanMatrix.E₆_off_diag_nonpos

added theorem CartanMatrix.E₆_transpose

added theorem CartanMatrix.E₇_off_diag_nonpos

added theorem CartanMatrix.E₇_transpose

added theorem CartanMatrix.E₈_off_diag_nonpos

added theorem CartanMatrix.E₈_transpose

added theorem CartanMatrix.F₄_off_diag_nonpos

added theorem CartanMatrix.G₂_off_diag_nonpos