OAI/NumberTheory/PowerFree/MediumDegree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.norm_indexed_count line 11
  2. theorem OAI.QuarticPowerFree.norm_onebox_exponents line 103
  3. theorem OAI.QuarticPowerFree.balanced_coordinates_onebox line 142
  4. theorem OAI.QuarticPowerFree.large_prime_power_upper line 183
  5. theorem OAI.QuarticPowerFree.medium_degree_dyadic_tail line 200
  6. theorem OAI.QuarticPowerFree.density_ge_five line 251
  7. structure OAI.QuarticPowerFree.QuarticBoxSystem line 269
  8. def OAI.QuarticPowerFree.QuarticBoxSystem.a line 290
  9. def OAI.QuarticPowerFree.QuarticBoxSystem.equation line 293
  10. def OAI.QuarticPowerFree.QuarticBoxSystem.ideal line 295
  11. theorem OAI.QuarticPowerFree.QuarticBoxSystem.quotient_equations line 298
  12. theorem OAI.QuarticPowerFree.QuarticBoxSystem.quotient_left_nonzero line 310
  13. theorem OAI.QuarticPowerFree.QuarticBoxSystem.right_real_weight line 321