OAI/NumberTheory/EgyptianFractions/CoordinateBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.DenominatorArithmetic.unit_den line 9
2. lemma OAI.Problem337.DenominatorArithmetic.sum_unit_den_dvd_prod line 12
3. lemma OAI.Problem337.DenominatorArithmetic.one_div_den_le line 24
4. lemma OAI.Problem337.DenominatorArithmetic.one_div_prod_le_remainder line 32
5. lemma OAI.Problem337.DenominatorArithmetic.denominator_le_length_mul_prefix line 49
6. lemma OAI.Problem337.DenominatorArithmetic.sum_two_pow_Iio line 94
7. theorem OAI.Problem337.DenominatorArithmetic.ordered_unit_denominator_bound line 112