OAI/MathematicalPhysics/Heisenberg/ExchangeCycles.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.LayeredExchange.forwardHom_subtype line 19
  2. lemma OAI.Heisenberg.LayeredExchange.forwardHom_reindex line 33
  3. lemma OAI.Heisenberg.LayeredExchange.determinantLaw_holes line 42
  4. lemma OAI.Heisenberg.LayeredExchange.determinantLaw_reindexed line 51
  5. abbrev OAI.Heisenberg.Cycle.Classes line 67
  6. def OAI.Heisenberg.Cycle.classOf line 68
  7. lemma OAI.Heisenberg.Cycle.classOf_eq_iff line 69
  8. lemma OAI.Heisenberg.Cycle.classOf_apply line 71
  9. abbrev OAI.Heisenberg.Cycle.MissingClasses line 74
  10. def OAI.Heisenberg.Cycle.missingCount line 76
  11. def OAI.Heisenberg.Cycle.colorSpace line 79
  12. lemma OAI.Heisenberg.Cycle.colorSpace_mem line 89
  13. lemma OAI.Heisenberg.Cycle.color_eq_of_sameCycle line 94
  14. def OAI.Heisenberg.Cycle.colorEquiv line 104
  15. theorem OAI.Heisenberg.Cycle.card_colorSpace line 131
  16. lemma OAI.Heisenberg.Cycle.finrank_comparison line 137
  17. theorem OAI.Heisenberg.Cycle.missingCount_swap_le line 157
  18. theorem OAI.Heisenberg.Cycle.weight_swap_le line 186
  19. def OAI.Heisenberg.Cycle.MissingSet line 198
  20. lemma OAI.Heisenberg.Cycle.missing_apply line 202
  21. lemma OAI.Heisenberg.Cycle.missing_disjoint_pins line 207
  22. lemma OAI.Heisenberg.Cycle.color_zero_not_missing line 212
  23. theorem OAI.Heisenberg.Cycle.missing_weight_rigid line 218
  24. lemma OAI.Heisenberg.Cycle.exposed_subset_missing line 247
  25. def OAI.Heisenberg.Cycle.OutsideHit line 261
  26. lemma OAI.Heisenberg.Cycle.sameMissing_iff_outsideHit line 264