OAI/NumberTheory/PowerFree/PrincipalLifts.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.pairLeft line 10
  2. def OAI.QuarticPowerFree.pairRight line 14
  3. theorem OAI.QuarticPowerFree.pairEvaluation_left line 18
  4. theorem OAI.QuarticPowerFree.pairEvaluation_right line 25
  5. theorem OAI.QuarticPowerFree.pairCoeffMap_scalar line 32
  6. def OAI.QuarticPowerFree.rootPairQ line 36
  7. abbrev OAI.QuarticPowerFree.RootPair line 40
  8. def OAI.QuarticPowerFree.coneDifference line 43
  9. abbrev OAI.QuarticPowerFree.PairAffine line 46
  10. def OAI.QuarticPowerFree.pairAffineMk line 50
  11. theorem OAI.QuarticPowerFree.pairAffineMk_t line 54
  12. def OAI.QuarticPowerFree.pairAffineLeft line 61
  13. def OAI.QuarticPowerFree.pairAffineRight line 65
  14. lemma OAI.QuarticPowerFree.pairAffine_equation line 69
  15. lemma OAI.QuarticPowerFree.rootPair_equation line 77
  16. def OAI.QuarticPowerFree.rootPairToAffine line 85
  17. def OAI.QuarticPowerFree.pairConeToRoot line 101
  18. theorem OAI.QuarticPowerFree.pairConeToRoot_t line 115
  19. theorem OAI.QuarticPowerFree.pairConeToRoot_left line 120
  20. theorem OAI.QuarticPowerFree.pairConeToRoot_right line 129
  21. def OAI.QuarticPowerFree.pairAffineToRoot line 138
  22. theorem OAI.QuarticPowerFree.pairAffineToRoot_mk line 147
  23. def OAI.QuarticPowerFree.pairCoeffHom line 152
  24. theorem OAI.QuarticPowerFree.rootPairToAffine_left line 157
  25. theorem OAI.QuarticPowerFree.rootPairToAffine_right line 163
  26. theorem OAI.QuarticPowerFree.pairAffineToRoot_left line 169
  27. theorem OAI.QuarticPowerFree.pairAffineToRoot_right line 175
  28. theorem OAI.QuarticPowerFree.pairAffineToRoot_leftInverse line 181
  29. theorem OAI.QuarticPowerFree.rootPairToAffine_comp_cone line 210
  30. theorem OAI.QuarticPowerFree.pairAffineToRoot_rightInverse line 247
  31. def OAI.QuarticPowerFree.rootPairAffineEquiv line 254
  32. theorem OAI.QuarticPowerFree.homogeneous_dehomogenization_zero line 264
  33. theorem OAI.QuarticPowerFree.homogeneous_dehomogenization_eq line 294
  34. theorem OAI.QuarticPowerFree.saturated_homogeneous_minimal_degree line 307
  35. theorem OAI.QuarticPowerFree.pairAffine_divisor_bounded_lift line 330