OAI/Combinatorics/MatchingCount/Machines/TreeSum.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.TreeTyped.sumRep line 9
2. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 12) line 12
3. def OAI.MatchingFPRAS.TreeTyped.inl line 14
4. def OAI.MatchingFPRAS.TreeTyped.inr line 16
5. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_inl line 19
6. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_inr line 24
7. def OAI.MatchingFPRAS.TreeTyped.sumCases line 29
8. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_sumCases line 36
9. def OAI.MatchingFPRAS.TreeTyped.sumEqual line 44
10. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_sumEqual line 52
11. def OAI.MatchingFPRAS.TreeTyped.sumLexLe line 64
12. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_sumLexLe line 72
13. def OAI.MatchingFPRAS.TreeTyped.optionRep line 86
14. instance OAI.MatchingFPRAS.TreeTyped.(instance at line 89) line 89
15. def OAI.MatchingFPRAS.TreeTyped.some line 90
16. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_some line 93
17. def OAI.MatchingFPRAS.TreeTyped.optionCases line 98
18. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_optionCases line 104