OAI/NumberTheory/PowerFree/PositiveCoordinates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.positiveExponent line 11
  2. def OAI.QuarticPowerFree.positiveLaurentMap line 16
  3. theorem OAI.QuarticPowerFree.positiveLaurentMap_monomial line 20
  4. theorem OAI.QuarticPowerFree.positiveLaurentMap_C line 25
  5. theorem OAI.QuarticPowerFree.positiveLaurentMap_X line 30
  6. theorem OAI.QuarticPowerFree.positiveLaurentMap_injective line 39
  7. theorem OAI.QuarticPowerFree.positiveLaurentMap_prod_X line 47
  8. theorem OAI.QuarticPowerFree.positiveLaurent_fractions line 57
  9. theorem OAI.QuarticPowerFree.positiveLaurent_isLocalization line 88
  10. def OAI.QuarticPowerFree.positiveToPair line 122
  11. theorem OAI.QuarticPowerFree.positiveToPair_C line 126
  12. theorem OAI.QuarticPowerFree.positiveToPair_X line 131
  13. theorem OAI.QuarticPowerFree.positiveToPair_toLaurent line 136
  14. theorem OAI.QuarticPowerFree.pair_laurent_evaluation line 144
  15. theorem OAI.QuarticPowerFree.positiveLaurent_kernel line 175
  16. theorem OAI.QuarticPowerFree.rootPair_projection_kernel line 206
  17. theorem OAI.QuarticPowerFree.homogeneous_aeval_monomial line 262
  18. theorem OAI.QuarticPowerFree.polynomial_homogeneous_lift line 285