OAI/NumberTheory/PowerFree/PairCuts.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuarticPowerFree.PairBasisIndex line 7
  2. def OAI.QuarticPowerFree.pairIndexToTuple line 10
  3. def OAI.QuarticPowerFree.tupleBasisIndex line 13
  4. def OAI.QuarticPowerFree.pairBasisWeight line 19
  5. theorem OAI.QuarticPowerFree.pairIndexToTuple_normal line 23
  6. theorem OAI.QuarticPowerFree.pairBasisWeight_eq line 28
  7. theorem OAI.QuarticPowerFree.pairIndexToTuple_tupleBasisIndex line 40
  8. theorem OAI.QuarticPowerFree.tupleBasisIndex_pairIndexToTuple line 48
  9. def OAI.QuarticPowerFree.pairBasisWeightEquiv line 57
  10. abbrev OAI.QuarticPowerFree.PairCone line 84
  11. def OAI.QuarticPowerFree.pairConeScale line 87
  12. def OAI.QuarticPowerFree.pairConeBasis line 93
  13. theorem OAI.QuarticPowerFree.pairConeBasis_homogeneous line 99
  14. theorem OAI.QuarticPowerFree.pairCone_finite line 107
  15. theorem OAI.QuarticPowerFree.pairCone_finrank line 115
  16. theorem OAI.QuarticPowerFree.pairCone_cut_hilbert line 125
  17. def OAI.QuarticPowerFree.pairMap line 153
  18. theorem OAI.QuarticPowerFree.pairMap_mk line 170
  19. def OAI.QuarticPowerFree.pairCoeffMap line 175
  20. theorem OAI.QuarticPowerFree.pairMap_eq_zero_iff_dvd line 179
  21. theorem OAI.QuarticPowerFree.pairCoeff_span_isPrime line 210
  22. theorem OAI.QuarticPowerFree.pairCoeffMap_injective line 224
  23. def OAI.QuarticPowerFree.eraseVariable line 238
  24. theorem OAI.QuarticPowerFree.eraseVariable_X line 243
  25. theorem OAI.QuarticPowerFree.eraseVariable_C line 248
  26. theorem OAI.QuarticPowerFree.X_dvd_sub_eraseVariable line 251
  27. theorem OAI.QuarticPowerFree.eraseVariable_eq_zero_iff line 265
  28. theorem OAI.QuarticPowerFree.dvd_of_dvd_prime_mul line 274
  29. theorem OAI.QuarticPowerFree.dvd_of_dvd_coordinate_mul line 285
  30. theorem OAI.QuarticPowerFree.principal_under_map_coordinates line 298
  31. theorem OAI.QuarticPowerFree.principal_isPrime_of_localization_coordinates line 313
  32. theorem OAI.QuarticPowerFree.principal_saturated_power line 323
  33. theorem OAI.QuarticPowerFree.saturated_quotient_localization_injective line 332
  34. theorem OAI.QuarticPowerFree.homogeneous_dehomogenization_kernel line 348
  35. theorem OAI.QuarticPowerFree.homogeneous_dehomogenization_finrank line 394
  36. theorem OAI.QuarticPowerFree.pairCone_t_prime line 422
  37. theorem OAI.QuarticPowerFree.pairScale_coeff line 441
  38. theorem OAI.QuarticPowerFree.pairCone_t_homogeneous line 450
  39. theorem OAI.QuarticPowerFree.pairAffine_cut_hilbert line 457