Commit 2024-04-04 21:40 aca0073f

View on Github →

feat(GroupTheory/Coxeter): decidability (#11879)

Estimated changes

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/Coxeter/Matrix.lean

modified theorem CoxeterMatrix.E₆IsCoxeter

modified theorem CoxeterMatrix.E₇IsCoxeter

modified theorem CoxeterMatrix.E₈IsCoxeter

modified theorem CoxeterMatrix.F₄IsCoxeter

modified theorem CoxeterMatrix.G₂IsCoxeter

modified theorem CoxeterMatrix.H₃IsCoxeter

modified theorem CoxeterMatrix.H₄IsCoxeter