OAI/Topology/ArtinGroups/Harmonic/ReducedExpression.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.wordArtin_altList line 12
  2. lemma OAI.HarmonicArtin.wordArtin_braid line 21
  3. theorem OAI.HarmonicArtin.wordArtin_eq_of_reduced line 26
  4. def OAI.HarmonicArtin.reducedExpression line 35
  5. lemma OAI.HarmonicArtin.reducedExpression_reduced line 38
  6. lemma OAI.HarmonicArtin.wordCoxeter_reducedExpression line 42
  7. def OAI.HarmonicArtin.positiveLift line 46
  8. lemma OAI.HarmonicArtin.positiveLift_word line 49
  9. lemma OAI.HarmonicArtin.positiveLift_one line 55
  10. lemma OAI.HarmonicArtin.wordArtin_append line 59
  11. lemma OAI.HarmonicArtin.positiveLift_mul line 63
  12. lemma OAI.HarmonicArtin.wordArtin_mem_parabolic line 83
  13. lemma OAI.HarmonicArtin.positiveLift_mem_parabolic line 92