OAI/Topology/ArtinGroups/Geometry/RootPair.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.Geometric.rootPair line 14
  2. lemma OAI.HarmonicArtin.Geometric.rootPair_symm line 17
  3. lemma OAI.HarmonicArtin.Geometric.rootPair_sub_left line 27
  4. lemma OAI.HarmonicArtin.Geometric.rootPair_sub_right line 31
  5. lemma OAI.HarmonicArtin.Geometric.rootPair_smul_left line 35
  6. lemma OAI.HarmonicArtin.Geometric.rootPair_smul_right line 39
  7. lemma OAI.HarmonicArtin.Geometric.rootPair_basis_left line 43
  8. lemma OAI.HarmonicArtin.Geometric.rootPair_basis_right line 47
  9. lemma OAI.HarmonicArtin.Geometric.reflection_rootPair line 51
  10. lemma OAI.HarmonicArtin.Geometric.representation_rootPair line 58
  11. lemma OAI.HarmonicArtin.Geometric.rootRow_representation line 66
  12. lemma OAI.HarmonicArtin.Geometric.rootPair_pos line 73
  13. lemma OAI.HarmonicArtin.Geometric.rootPair_nonpos line 84
  14. lemma OAI.HarmonicArtin.Geometric.inverse_right_length line 90
  15. theorem OAI.HarmonicArtin.Geometric.rootRow_pos_iff_left_ascent line 94
  16. theorem OAI.HarmonicArtin.Geometric.chamber_stabilizer line 111