OAI/Topology/ArtinGroups/Quivers/ReversibleQuiver.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HarmonicArtin.ReversibleQuiver line 7
  2. theorem OAI.HarmonicArtin.ReversibleQuiver.reverse_reverse_apply line 19
  3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag line 22
  4. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 28) line 28
  5. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 31) line 31
  6. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex line 34
  7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow line 35
  8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token line 36
  9. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.ext line 38
  10. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_add line 42
  11. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_add line 44
  12. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_add line 46
  13. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_smul line 48
  14. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_smul line 50
  15. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_smul line 52
  16. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_zero line 54
  17. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_zero line 55
  18. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_zero line 56
  19. def OAI.HarmonicArtin.ReversibleQuiver.leftScale line 64
  20. def OAI.HarmonicArtin.ReversibleQuiver.rightScale line 66
  21. def OAI.HarmonicArtin.ReversibleQuiver.backtrack line 68
  22. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_add_left line 71
  23. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_add_right line 78
  24. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_zero_left line 85
  25. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_zero_right line 89
  26. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_leftScale line 93
  27. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_rightScale line 103
  28. theorem OAI.HarmonicArtin.ReversibleQuiver.backtrack_balance line 113
  29. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 120) line 120
  30. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 125) line 125
  31. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_mul line 127
  32. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_mul line 129
  33. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_mul line 131
  34. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertex_one line 134
  35. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrow_one line 136
  36. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.token_one line 138
  37. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_assoc line 140
  38. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.one_mul line 151
  39. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_one line 158
  40. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_add line 165
  41. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.add_mul line 174
  42. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.zero_mul line 183
  43. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_zero line 190
  44. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.(instance at line 197) line 197
  45. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace line 210
  46. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_add line 212
  47. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_zero line 216
  48. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.sum_backtrack line 219
  49. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_expression line 227
  50. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_comm line 233
  51. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.vertexBasis line 243
  52. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenBasis line 245
  53. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.arrowBasis line 247
  54. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_tokenBasis line 249
  55. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_vertexBasis line 254
  56. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_arrowBasis line 259
  57. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_nondegenerate_left line 264
  58. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_nondegenerate_right line 275
  59. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_smul_mul line 282
  60. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_mul_smul line 288
  61. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tracePairing line 292
  62. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tracePairing_apply line 304
  63. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tracePairing_symmetric line 307
  64. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tracePairing_nondegenerate line 310
  65. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.annihilate_positive_iff line 313
  66. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_triple_mul line 334