OAI/Topology/ArtinGroups/Coxeter/Parabolic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.CoxeterExchange.exists_reduced_subword line 9
2. def OAI.HarmonicArtin.CoxeterExchange.parabolic line 27
3. lemma OAI.HarmonicArtin.CoxeterExchange.simple_mem_parabolic line 29
4. lemma OAI.HarmonicArtin.CoxeterExchange.wordProd_mem_parabolic line 32
5. lemma OAI.HarmonicArtin.CoxeterExchange.mem_parabolic_iff_word line 41
6. lemma OAI.HarmonicArtin.CoxeterExchange.mem_parabolic_iff_reduced_word line 60
7. def OAI.HarmonicArtin.CoxeterExchange.IsParabolicMinimum line 71
8. lemma OAI.HarmonicArtin.CoxeterExchange.length_word_mul_of_minimum line 74
9. lemma OAI.HarmonicArtin.CoxeterExchange.length_mul_of_minimum line 124
10. lemma OAI.HarmonicArtin.CoxeterExchange.exists_parabolic_decomposition line 130
11. lemma OAI.HarmonicArtin.CoxeterExchange.parabolic_minimum_unique line 146
12. lemma OAI.HarmonicArtin.CoxeterExchange.descent_parabolic_factor line 157