Commit 2024-04-26 09:42 7ba4d203

View on Github →

feat: simple reflections, words, lifting in Coxeter groups (#11406) Prove basic properties of simple reflections in a Coxeter group. Add definitions CoxeterSystem.lift, and CoxeterSystem.wordProd to GroupTheory.Coxeter.Basic and prove their basic properties.

Estimated changes

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

added def CoxeterMatrix.IsLiftable

modified def CoxeterMatrix.relationsSet

added theorem CoxeterSystem.ext_simple

added theorem CoxeterSystem.inv_simple

added def CoxeterSystem.lift

added theorem CoxeterSystem.lift_apply_simple

added theorem CoxeterSystem.simple_determines_coxeterSystem

added theorem CoxeterSystem.simple_induction

added theorem CoxeterSystem.simple_induction_left

added theorem CoxeterSystem.simple_induction_right

added theorem CoxeterSystem.simple_mul_simple_cancel_left

added theorem CoxeterSystem.simple_mul_simple_cancel_right

added theorem CoxeterSystem.simple_mul_simple_pow'

added theorem CoxeterSystem.simple_mul_simple_pow

added theorem CoxeterSystem.simple_mul_simple_self

added theorem CoxeterSystem.simple_sq

added theorem CoxeterSystem.subgroup_closure_range_simple

added theorem CoxeterSystem.submonoid_closure_range_simple

added def CoxeterSystem.wordProd

added theorem CoxeterSystem.wordProd_append

added theorem CoxeterSystem.wordProd_concat

added theorem CoxeterSystem.wordProd_cons

added theorem CoxeterSystem.wordProd_nil

added theorem CoxeterSystem.wordProd_reverse

added theorem CoxeterSystem.wordProd_singleton

added theorem CoxeterSystem.wordProd_surjective