OAI/Topology/ArtinGroups/Geometry/RootNonposDescent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.Geometric.root_nonpos_iff_descent line 14
2. lemma OAI.HarmonicArtin.Geometric.vector_eq_sum_simple line 25
3. lemma OAI.HarmonicArtin.Geometric.representation_nonpos_of_columns line 29
4. theorem OAI.HarmonicArtin.Geometric.length_mul_of_all_descents line 39
5. lemma OAI.HarmonicArtin.Geometric.length_le_of_all_descents line 66
6. theorem OAI.HarmonicArtin.Geometric.finite_of_all_descents line 72
7. lemma OAI.HarmonicArtin.Geometric.exists_longest line 84
8. lemma OAI.HarmonicArtin.Geometric.all_descents_of_longest line 90
9. lemma OAI.HarmonicArtin.Geometric.all_left_descents_of_longest line 96