OAI/NumberTheory/PowerFree/LaurentCoordinates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.pairToLaurent line 11
  2. def OAI.QuarticPowerFree.pairCoordinate line 19
  3. theorem OAI.QuarticPowerFree.pairToLaurent_coordinate line 23
  4. theorem OAI.QuarticPowerFree.pairToLaurent_C line 29
  5. theorem OAI.QuarticPowerFree.pairToLaurent_injective line 35
  6. theorem OAI.QuarticPowerFree.pairToLaurent_prod_coordinate line 45
  7. theorem OAI.QuarticPowerFree.pairLaurent_fractions line 56
  8. theorem OAI.QuarticPowerFree.pairLaurent_isLocalization line 89
  9. theorem OAI.QuarticPowerFree.pair_coordinate_prime line 125
  10. theorem OAI.QuarticPowerFree.pair_root_coordinate_prime line 149
  11. theorem OAI.QuarticPowerFree.extract_finite_nonunit_factors line 164
  12. theorem OAI.QuarticPowerFree.extract_prime_equation_from_open line 188
  13. theorem OAI.QuarticPowerFree.rootPair_extract_prime_cut line 211
  14. def OAI.QuarticPowerFree.pairEvaluation line 255
  15. theorem OAI.QuarticPowerFree.pairEvaluation_mk line 267
  16. theorem OAI.QuarticPowerFree.pairEvaluation_coeff line 274
  17. theorem OAI.QuarticPowerFree.pairEvaluation_ext line 282
  18. theorem OAI.QuarticPowerFree.pairCoordinate_equation line 302