OAI/Topology/ArtinGroups/Quivers/StringArrow.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringArrow line 11
  2. def OAI.HarmonicArtin.ReversibleQuiver.StringArrow.base line 17
  3. def OAI.HarmonicArtin.ReversibleQuiver.StringArrow.left line 18
  4. def OAI.HarmonicArtin.ReversibleQuiver.StringArrow.right line 19
  5. lemma OAI.HarmonicArtin.ReversibleQuiver.StringArrow.ext line 21
  6. def OAI.HarmonicArtin.ReversibleQuiver.stringQuiver line 31
  7. abbrev OAI.HarmonicArtin.ReversibleQuiver.StringIndex line 61
  8. def OAI.HarmonicArtin.ReversibleQuiver.StringIndex.old line 65
  9. def OAI.HarmonicArtin.ReversibleQuiver.StringIndex.label line 66
  10. def OAI.HarmonicArtin.ReversibleQuiver.StringIndex.new line 67
  11. lemma OAI.HarmonicArtin.ReversibleQuiver.StringIndex.ext line 68
  12. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.coefficient line 80
  13. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.unitImage line 85
  14. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.tokenImage line 88
  15. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage line 91
  16. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.unitImage_mul line 101
  17. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.mul_unitImage line 112
  18. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_left line 122
  19. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_right line 146
  20. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.unitImage_arrowImage line 170
  21. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_unitImage line 192
  22. def OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.liftIndex line 214
  23. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.sum_over line 216
  24. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.reverse_base line 239
  25. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.reverse_left line 243
  26. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.reverse_right line 247
  27. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.reverse_eq_iff line 252
  28. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_eq_zero_left line 261
  29. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_eq_zero_right line 267
  30. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_entry_mul_of_not_reverse line 273
  31. lemma OAI.HarmonicArtin.ReversibleQuiver.StringFunctor.arrowImage_mul_of_not_reverse_base line 304