Theorem CartanMatrix.E₈_off_diag_nonpos

Modification history

2026-08-13 09:59
Mathlib/LinearAlgebra/Matrix/Cartan.lean
feat(LinearAlgebra/Matrix): add the generalized E-type Cartan matrix family (#42157) …
Modified CartanMatrix.E₈_off_diag_nonposView on Github →
2025-12-19 18:36
Mathlib/Data/Matrix/Cartan.lean
feat(Data/Matrix/Cartan): off-diagonal and transpose for exceptional matrices (#32998) …
Added CartanMatrix.E₈_off_diag_nonposView on Github →