OAI/Topology/ArtinGroups/Coxeter/ArtinCoxeter.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.artinCoxeter_relators line 12
  2. def OAI.HarmonicArtin.artinCoxeter line 18
  3. lemma OAI.HarmonicArtin.artinCoxeter_generator line 20
  4. lemma OAI.HarmonicArtin.artinCoxeter_word line 23
  5. lemma OAI.HarmonicArtin.artinCoxeter_positiveLift line 30
  6. lemma OAI.HarmonicArtin.positiveLift_injective line 34
  7. def OAI.HarmonicArtin.CoxeterCellFace line 37
  8. def OAI.HarmonicArtin.CoxeterCellFace.vertexSet line 43
  9. lemma OAI.HarmonicArtin.CoxeterCellFace.source_mem line 46
  10. lemma OAI.HarmonicArtin.CoxeterCellFace.vertices_subset_iff line 50
  11. instance OAI.HarmonicArtin.CoxeterCellFace.(instance at line 60) line 60
  12. lemma OAI.HarmonicArtin.CoxeterCellFace.le_iff line 78
  13. def OAI.HarmonicArtin.coxeterFaceToLifted line 89
  14. lemma OAI.HarmonicArtin.coxeterFaceToLifted_full line 93
  15. lemma OAI.HarmonicArtin.coxeterFaceToLifted_injective line 104
  16. lemma OAI.HarmonicArtin.coxeterFaceToLifted_le_iff line 110
  17. def OAI.HarmonicArtin.coxeterFacesClosedLiftedIso line 146