OAI/Combinatorics/TriangleRemoval/Spectral/WheelSpoke.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.cycleNext_val line 13
  2. lemma OAI.SharpTerminalLeave.cycleNext_injective line 22
  3. lemma OAI.SharpTerminalLeave.cycleNext_ne line 29
  4. lemma OAI.SharpTerminalLeave.cycleNext_twice_ne line 35
  5. def OAI.SharpTerminalLeave.wheelSpoke line 43
  6. def OAI.SharpTerminalLeave.wheelRim line 44
  7. lemma OAI.SharpTerminalLeave.wheelSpoke_injective line 46
  8. lemma OAI.SharpTerminalLeave.wheelRim_injective line 54
  9. lemma OAI.SharpTerminalLeave.wheelSpoke_ne_rim line 66
  10. def OAI.SharpTerminalLeave.wheelTemplate line 71
  11. lemma OAI.SharpTerminalLeave.wheelTemplate_roots_card line 93
  12. lemma OAI.SharpTerminalLeave.wheelTemplate_edges_card line 96
  13. lemma OAI.SharpTerminalLeave.wheelTemplate_balanced line 110
  14. def OAI.SharpTerminalLeave.wheelRoot line 138
  15. lemma OAI.SharpTerminalLeave.wheelRooted_zero line 148
  16. def OAI.SharpTerminalLeave.wheelRestrict line 152
  17. lemma OAI.SharpTerminalLeave.wheel_image_subset line 156
  18. lemma OAI.SharpTerminalLeave.wheelRestrict_injective line 182
  19. lemma OAI.SharpTerminalLeave.wheelRestrict_surj line 192
  20. theorem OAI.SharpTerminalLeave.wheel_rootedCount line 210
  21. theorem OAI.SharpTerminalLeave.wheel_rootedScaling line 237