Commit 2024-02-07 17:07 e4d4665e

View on Github →

feat(GroupTheory/SpecificGroups/Coxeter) : Add Coxeter Systems and Coxeter Groups (#8223) Coxeter Systems and Coxeter Groups

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/SpecificGroups/Coxeter.lean

added def CoxeterGroup.Relations.ofMatrix

added def CoxeterGroup.Relations.toSet

added def CoxeterGroup.of

added theorem CoxeterGroup.of_apply

added theorem CoxeterMatrix.AₙIsCoxeter

added theorem CoxeterMatrix.BₙIsCoxeter

added theorem CoxeterMatrix.DₙIsCoxeter

added def CoxeterMatrix.E₆

added theorem CoxeterMatrix.E₆IsCoxeter

added def CoxeterMatrix.E₇

added theorem CoxeterMatrix.E₇IsCoxeter

added def CoxeterMatrix.E₈

added theorem CoxeterMatrix.E₈IsCoxeter

added def CoxeterMatrix.F₄

added theorem CoxeterMatrix.F₄IsCoxeter

added def CoxeterMatrix.G₂

added theorem CoxeterMatrix.G₂IsCoxeter

added def CoxeterMatrix.H₃

added theorem CoxeterMatrix.H₃IsCoxeter

added def CoxeterMatrix.H₄

added theorem CoxeterMatrix.H₄IsCoxeter

added theorem CoxeterMatrix.I₂ₘIsCoxeter

added def CoxeterSystem.equivCoxeterGroup

added theorem CoxeterSystem.equivCoxeterGroup_apply_of

added theorem CoxeterSystem.equivCoxeterGroup_symm_apply_of

added theorem CoxeterSystem.ext'

added theorem CoxeterSystem.ext

added theorem CoxeterSystem.map_apply

added theorem CoxeterSystem.map_relations_eq_reindex_relations

added theorem CoxeterSystem.mulEquiv_apply_coe

added def CoxeterSystem.ofCoxeterGroup

added theorem CoxeterSystem.ofCoxeterGroup_apply

added theorem CoxeterSystem.reindex_apply

added structure CoxeterSystem

added def Matrix.CoxeterGroup

added structure Matrix.IsCoxeter