OAI/NumberTheory/PowerFree/QuarticComponents.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.quarticA line 10
  2. def OAI.QuarticPowerFree.quarticB line 11
  3. def OAI.QuarticPowerFree.quarticNumerator line 12
  4. def OAI.QuarticPowerFree.quarticEnvelope line 15
  5. def OAI.QuarticPowerFree.quarticU line 16
  6. def OAI.QuarticPowerFree.quarticV line 17
  7. def OAI.QuarticPowerFree.quarticStage line 18
  8. def OAI.QuarticPowerFree.quarticIncrement line 19
  9. lemma OAI.QuarticPowerFree.quarticA_pos line 22
  10. lemma OAI.QuarticPowerFree.quarticB_pos line 23
  11. lemma OAI.QuarticPowerFree.quarticU_pos line 24
  12. lemma OAI.QuarticPowerFree.quarticV_pos line 25
  13. lemma OAI.QuarticPowerFree.quarticEnvelope_pos line 26
  14. lemma OAI.QuarticPowerFree.quarticU_le line 28
  15. lemma OAI.QuarticPowerFree.quarticV_le line 32
  16. lemma OAI.QuarticPowerFree.quartic_full_nat line 37
  17. lemma OAI.QuarticPowerFree.quartic_generic_nat line 40
  18. lemma OAI.QuarticPowerFree.quartic_affine_nat line 43
  19. lemma OAI.QuarticPowerFree.quartic_pole_nat line 46
  20. lemma OAI.QuarticPowerFree.quartic_increment_nonneg line 50
  21. lemma OAI.QuarticPowerFree.quartic_prefix line 53
  22. lemma OAI.QuarticPowerFree.quartic_sum line 57
  23. lemma OAI.QuarticPowerFree.quartic_generic_rat line 62
  24. lemma OAI.QuarticPowerFree.quartic_full_rat line 66
  25. lemma OAI.QuarticPowerFree.quartic_affine_rat line 69
  26. lemma OAI.QuarticPowerFree.quartic_pole_rat line 72
  27. lemma OAI.QuarticPowerFree.quartic_curve_rat line 75
  28. lemma OAI.QuarticPowerFree.quartic_generic_threshold line 79
  29. lemma OAI.QuarticPowerFree.quartic_full_threshold line 92
  30. lemma OAI.QuarticPowerFree.quartic_affine_threshold line 101
  31. lemma OAI.QuarticPowerFree.quartic_pole_threshold line 109
  32. lemma OAI.QuarticPowerFree.quartic_curve_threshold line 116
  33. theorem OAI.QuarticPowerFree.quartic_generic_threshold_uniform line 127
  34. theorem OAI.QuarticPowerFree.quartic_full_threshold_uniform line 159
  35. theorem OAI.QuarticPowerFree.quartic_component_alternatives line 188