Commit 2024-05-11 18:18 0e70892c

View on Github →

feat: length, reduced words in Coxeter groups (#11465) Add new file GroupTheory/Coxeter/Length.lean. Define the length function and reduced words of Coxeter groups. Prove their basic properties. I decided to split #11408 (now closed) into two pull requests. This is the first one.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

added def CoxeterSystem.alternatingWord

added theorem CoxeterSystem.alternatingWord_succ'

added theorem CoxeterSystem.alternatingWord_succ

added theorem CoxeterSystem.length_alternatingWord

added theorem CoxeterSystem.prod_alternatingWord_eq_mul_pow

added theorem CoxeterSystem.prod_alternatingWord_eq_prod_alternatingWord_sub

added theorem CoxeterSystem.wordProd_braidWord_eq

Created Mathlib/GroupTheory/Coxeter/Length.lean

added def CoxeterSystem.IsLeftDescent

added def CoxeterSystem.IsReduced

added def CoxeterSystem.IsRightDescent

added theorem CoxeterSystem.exists_leftDescent_of_ne_one

added theorem CoxeterSystem.exists_reduced_word'

added theorem CoxeterSystem.exists_reduced_word

added theorem CoxeterSystem.exists_rightDescent_of_ne_one

added theorem CoxeterSystem.isLeftDescent_iff

added theorem CoxeterSystem.isLeftDescent_iff_not_isLeftDescent_mul

added theorem CoxeterSystem.isLeftDescent_inv_iff

added theorem CoxeterSystem.isReduced_drop

added theorem CoxeterSystem.isReduced_reverse

added theorem CoxeterSystem.isReduced_take

added theorem CoxeterSystem.isRightDescent_iff

added theorem CoxeterSystem.isRightDescent_iff_not_isRightDescent_mul

added theorem CoxeterSystem.isRightDescent_inv_iff

added def CoxeterSystem.lengthParity

added theorem CoxeterSystem.lengthParity_comp_simple

added theorem CoxeterSystem.lengthParity_eq_ofAdd_length

added theorem CoxeterSystem.lengthParity_simple

added theorem CoxeterSystem.length_eq_one_iff

added theorem CoxeterSystem.length_eq_zero_iff

added theorem CoxeterSystem.length_inv

added theorem CoxeterSystem.length_mul_ge_length_sub_length'

added theorem CoxeterSystem.length_mul_ge_length_sub_length

added theorem CoxeterSystem.length_mul_ge_max

added theorem CoxeterSystem.length_mul_le

added theorem CoxeterSystem.length_mul_mod_two

added theorem CoxeterSystem.length_mul_simple

added theorem CoxeterSystem.length_mul_simple_ne

added theorem CoxeterSystem.length_one

added theorem CoxeterSystem.length_simple

added theorem CoxeterSystem.length_simple_mul

added theorem CoxeterSystem.length_simple_mul_ne

added theorem CoxeterSystem.length_wordProd_le

added theorem CoxeterSystem.not_isLeftDescent_iff

added theorem CoxeterSystem.not_isLeftDescent_one

added theorem CoxeterSystem.not_isReduced_alternatingWord

added theorem CoxeterSystem.not_isRightDescent_iff

added theorem CoxeterSystem.not_isRightDescent_one

Modified docs/references.bib