OAI/Combinatorics/ParityLifts/RootedTests.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ParityWL.RootedTest line 15

    Source documentation

    Sources may have loops during root gluing. A loop contributes zero on every simple target; it is never silently deleted.

    structure RootedTest (k t : ℕ) where
…
  2. def OAI.ParityWL.RelationMaps line 28
  3. instance OAI.ParityWL.relationMapsFintype line 31
  4. def OAI.ParityWL.RootedTest.Maps line 36
  5. instance OAI.ParityWL.rootedMapsFintype line 40
  6. def OAI.ParityWL.RootedTest.count line 45
  7. def OAI.ParityWL.RootedTest.totalEquiv line 49
  8. lemma OAI.ParityWL.RootedTest.sum_count line 61
  9. def OAI.ParityWL.relationMapsSimpleEquiv line 67
  10. lemma OAI.ParityWL.relationMaps_loop line 74
  11. lemma OAI.ParityWL.no_choice_equal_relation line 80
  12. lemma OAI.ParityWL.no_choice_equal_rooted_total line 95
  13. def OAI.ParityWL.singleBagTest line 101
  14. def OAI.ParityWL.isolatedTest line 129
  15. lemma OAI.ParityWL.isolatedTest_count line 133