OAI/Topology/ArtinGroups/Geometry/CartanForm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.Geometric.cartanForm line 15
2. lemma OAI.HarmonicArtin.Geometric.cartanForm_symm line 17
3. lemma OAI.HarmonicArtin.Geometric.cartanForm_single_left line 27
4. lemma OAI.HarmonicArtin.Geometric.cartanForm_single_right line 31
5. lemma OAI.HarmonicArtin.Geometric.cartanForm_reflection line 35
6. lemma OAI.HarmonicArtin.Geometric.cartanForm_invariant line 48
7. lemma OAI.HarmonicArtin.Geometric.positive_root_sum_ge_one line 59
8. lemma OAI.HarmonicArtin.Geometric.length_sum_bound line 92
9. theorem OAI.HarmonicArtin.Geometric.finite_of_cartan_posDef line 119