OAI/Probability/SwitchChain/MatchingCount.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.MatchingCount.FixedPointFreeInvolution line 9
  2. instance OAI.Problem315.MatchingCount.(instance at line 12) line 12
  3. theorem OAI.Problem315.MatchingCount.involution_fin_four_card line 18
  4. def OAI.Problem315.MatchingCount.involutionCongr line 22
  5. theorem OAI.Problem315.MatchingCount.involution_card_of_card_four line 45
  6. theorem OAI.Problem315.MatchingCount.matching_neighbor_mem line 54
  7. def OAI.Problem315.MatchingCount.mate line 59
  8. theorem OAI.Problem315.MatchingCount.mate_adj line 63
  9. theorem OAI.Problem315.MatchingCount.mate_unique line 67
  10. def OAI.Problem315.MatchingCount.matchingToInvolution line 71
  11. def OAI.Problem315.MatchingCount.involutionGraph line 82
  12. def OAI.Problem315.MatchingCount.involutionToMatching line 94
  13. def OAI.Problem315.MatchingCount.matchingEquivInvolution line 106
  14. theorem OAI.Problem315.MatchingCount.perfectMatching_card line 134
  15. theorem OAI.Problem315.MatchingCount.orderedMatchings_card line 139
  16. theorem OAI.Problem315.MatchingCount.fourSet_card line 153
  17. theorem OAI.Problem315.MatchingCount.switchProposal_card line 158
  18. theorem OAI.Problem315.MatchingCount.allProposals_card line 169