OAI/Combinatorics/MatchingCount/Arithmetic/TreeFraction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.TreeFraction.Fraction line 9
  2. def OAI.MatchingFPRAS.TreeFraction.val line 10
  3. def OAI.MatchingFPRAS.TreeFraction.repr line 11
  4. def OAI.MatchingFPRAS.TreeFraction.normalize line 13
  5. def OAI.MatchingFPRAS.TreeFraction.normalizeRealizer line 16
  6. lemma OAI.MatchingFPRAS.TreeFraction.normalize_repr line 22
  7. lemma OAI.MatchingFPRAS.TreeFraction.val_nonneg line 29
  8. lemma OAI.MatchingFPRAS.TreeFraction.val_repr line 30
  9. lemma OAI.MatchingFPRAS.TreeFraction.normalize_val line 37
  10. lemma OAI.MatchingFPRAS.TreeFraction.normalize_den_pos line 41
  11. lemma OAI.MatchingFPRAS.TreeFraction.normalize_size_num line 44
  12. lemma OAI.MatchingFPRAS.TreeFraction.normalize_size_den line 48
  13. def OAI.MatchingFPRAS.TreeFraction.mul line 53
  14. def OAI.MatchingFPRAS.TreeFraction.mulRealizer line 54
  15. lemma OAI.MatchingFPRAS.TreeFraction.mul_val line 57
  16. def OAI.MatchingFPRAS.TreeFraction.add line 62
  17. def OAI.MatchingFPRAS.TreeFraction.addRealizer line 64
  18. lemma OAI.MatchingFPRAS.TreeFraction.add_val line 69
  19. def OAI.MatchingFPRAS.TreeFraction.div line 77
  20. def OAI.MatchingFPRAS.TreeFraction.divRealizer line 78
  21. lemma OAI.MatchingFPRAS.TreeFraction.div_val line 81
  22. def OAI.MatchingFPRAS.TreeFraction.less line 87
  23. def OAI.MatchingFPRAS.TreeFraction.lessRealizer line 88
  24. lemma OAI.MatchingFPRAS.TreeFraction.less_val line 91