OAI/Topology/ArtinGroups/Coxeter/ParabolicLongest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.IsParabolicLongest line 12
2. lemma OAI.HarmonicArtin.exists_parabolic_longest line 16
3. lemma OAI.HarmonicArtin.parabolic_longest_length_mul line 26
4. lemma OAI.HarmonicArtin.parabolic_longest_inverse line 42
5. lemma OAI.HarmonicArtin.parabolic_longest_complement_minimum line 48
6. theorem OAI.HarmonicArtin.lifted_top_face line 63
7. theorem OAI.HarmonicArtin.lifted_same_top_le line 88