OAI/Combinatorics/MatchingCount/Machines/TreeNaturalComb.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.TreeTyped.successor line 10
2. def OAI.MatchingFPRAS.TreeTyped.quotient line 13
3. def OAI.MatchingFPRAS.TreeTyped.remainder line 14
4. def OAI.MatchingFPRAS.TreeTyped.factStep line 16
5. lemma OAI.MatchingFPRAS.TreeTyped.fact_countDown line 17
6. def OAI.MatchingFPRAS.TreeTyped.factorial line 25
7. def OAI.MatchingFPRAS.TreeTyped.natChoose line 32
8. def OAI.MatchingFPRAS.TreeTyped.pairingStep line 48
9. lemma OAI.MatchingFPRAS.TreeTyped.pairing_range line 49
10. def OAI.MatchingFPRAS.TreeTyped.pairingNumber line 58