OAI/NumberTheory/SingleFold/Duplication.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SingleFold.DuplicationBound.gcd_numerator_divides line 7
2. lemma OAI.SingleFold.DuplicationBound.common_divisor_bound line 39
3. def OAI.SingleFold.DuplicationBound.height line 43
4. def OAI.SingleFold.DuplicationBound.dupX line 45
5. lemma OAI.SingleFold.DuplicationBound.dupX_fraction line 47
6. lemma OAI.SingleFold.DuplicationBound.height_dup_lower line 55
7. lemma OAI.SingleFold.DuplicationBound.denominator_square line 99
8. lemma OAI.SingleFold.DuplicationBound.bounded_points line 125
9. lemma OAI.SingleFold.DuplicationBound.small_points line 130
10. lemma OAI.SingleFold.DuplicationBound.height_dup_strict line 166
11. lemma OAI.SingleFold.DuplicationBound.height_dup_gt_five line 190
12. lemma OAI.SingleFold.DuplicationBound.height_y_zero line 204