OAI/Combinatorics/MatchingCount/Arithmetic/TreeGCD.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.digits line 10
  2. def OAI.MatchingFPRAS.TreeTyped.bitSize line 15
  3. def OAI.MatchingFPRAS.TreeTyped.sortedPair line 18
  4. def OAI.MatchingFPRAS.TreeTyped.sortedPairRealizer line 19
  5. lemma OAI.MatchingFPRAS.TreeTyped.sortedPair_order line 22
  6. lemma OAI.MatchingFPRAS.TreeTyped.sortedPair_gcd line 24
  7. lemma OAI.MatchingFPRAS.TreeTyped.sortedPair_size line 26
  8. def OAI.MatchingFPRAS.TreeTyped.gcdStep line 32
  9. def OAI.MatchingFPRAS.TreeTyped.gcdStepRealizer line 33
  10. lemma OAI.MatchingFPRAS.TreeTyped.mod_size_lt line 37
  11. lemma OAI.MatchingFPRAS.TreeTyped.gcdStep_order line 51
  12. lemma OAI.MatchingFPRAS.TreeTyped.gcdStep_gcd line 55
  13. lemma OAI.MatchingFPRAS.TreeTyped.gcdStep_decrease line 59
  14. def OAI.MatchingFPRAS.TreeTyped.gcdIterStep line 65
  15. lemma OAI.MatchingFPRAS.TreeTyped.gcdIter_zero line 66
  16. lemma OAI.MatchingFPRAS.TreeTyped.gcdIter_result line 71
  17. def OAI.MatchingFPRAS.TreeTyped.gcd line 88