OAI/Topology/ArtinGroups/Harmonic/UnfoldedHom.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicArtin.fusionExpandedWord_append line 13
  2. lemma OAI.HarmonicArtin.fusionExpandedWord_flatten_replicate line 17
  3. lemma OAI.HarmonicArtin.wordProd_flatten_replicate line 24
  4. def OAI.HarmonicArtin.unfoldedHom line 33
  5. lemma OAI.HarmonicArtin.unfoldedHom_simple line 53
  6. lemma OAI.HarmonicArtin.unfoldedHom_wordProd line 58
  7. theorem OAI.HarmonicArtin.unfolded_word_eq line 69
  8. theorem OAI.HarmonicArtin.unfoldedHom_left_ascent line 76
  9. theorem OAI.HarmonicArtin.unfoldedHom_right_ascent line 87
  10. theorem OAI.HarmonicArtin.unfoldedHom_right_descent line 100
  11. theorem OAI.HarmonicArtin.unfolded_finite line 113
  12. theorem OAI.HarmonicArtin.unfolded_longest line 122