Theorem CartanMatrix.E₈_det

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₈_detView on Github →
2026-07-27 08:26
Mathlib/LinearAlgebra/Matrix/Cartan.lean
fix(Tactic/NormDet): make norm_det proofs compatible with modules (#42119) …
Added CartanMatrix.E₈_detView on Github →