OAI/NumberTheory/PowerFree/QuarticBoxes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuarticPowerFree.quartic_box_prime_count line 11
2. theorem OAI.QuarticPowerFree.quartic_box_prime_count_unrestricted line 86
3. theorem OAI.QuarticPowerFree.quartic_box_count line 121
4. def OAI.QuarticPowerFree.quarticBoxWeight line 180
5. def OAI.QuarticPowerFree.quarticBoxNatWeight line 182
6. lemma OAI.QuarticPowerFree.quarticBoxWeight_pos line 184
7. lemma OAI.QuarticPowerFree.quarticBoxWeight_le line 188
8. lemma OAI.QuarticPowerFree.quarticBoxNatWeight_ne line 192
9. lemma OAI.QuarticPowerFree.quarticBoxWeight_scale line 196
10. def OAI.QuarticPowerFree.quarticBoxOfChart line 199
11. theorem OAI.QuarticPowerFree.quarticIntegralPoint_equation line 227
12. lemma OAI.QuarticPowerFree.prime_rational_fourth_ratio line 264
13. lemma OAI.QuarticPowerFree.IntegralEmbeddingChart.proportional_rat line 291
14. lemma OAI.QuarticPowerFree.prime_norm_proportional_sign line 323