OAI/Topology/ArtinGroups/Harmonic/PositiveDegreeHom.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.positive_word_surjective line 12
  2. lemma OAI.HarmonicArtin.positiveDegree_relations line 16
  3. def OAI.HarmonicArtin.positiveDegreeHom line 22
  4. def OAI.HarmonicArtin.positiveDegree line 25
  5. lemma OAI.HarmonicArtin.positiveDegree_one line 27
  6. lemma OAI.HarmonicArtin.positiveDegree_generator line 28
  7. lemma OAI.HarmonicArtin.positiveDegree_mul line 29
  8. lemma OAI.HarmonicArtin.positiveDegree_word line 34
  9. lemma OAI.HarmonicArtin.positiveDegree_zero_iff line 41
  10. lemma OAI.HarmonicArtin.positiveToCoxeter_relations line 48
  11. def OAI.HarmonicArtin.positiveToCoxeter line 53
  12. lemma OAI.HarmonicArtin.positiveToCoxeter_generator line 56
  13. lemma OAI.HarmonicArtin.positiveToCoxeter_word line 59
  14. lemma OAI.HarmonicArtin.positiveToCoxeter_length_le line 67
  15. def OAI.HarmonicArtin.positiveSimpleLift line 73
  16. lemma OAI.HarmonicArtin.positiveDegree_simpleLift line 76
  17. lemma OAI.HarmonicArtin.positiveToCoxeter_simpleLift line 82
  18. lemma OAI.HarmonicArtin.positiveSimpleLift_word line 86
  19. lemma OAI.HarmonicArtin.positive_eq_simpleLift_of_degree line 90