OAI/NumberTheory/PowerFree/SelectedPrimes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.primitive_map_zmod_ne_zero line 11
  2. theorem OAI.QuarticPowerFree.selected_constant_prime_count line 24
  3. def OAI.QuarticPowerFree.pointEvaluation line 65
  4. theorem OAI.QuarticPowerFree.pointEvaluation_X line 72
  5. theorem OAI.QuarticPowerFree.coordinate_constant_at_point line 78
  6. theorem OAI.QuarticPowerFree.rational_coordinate_at_point line 85
  7. theorem OAI.QuarticPowerFree.rational_selected_count line 96
  8. theorem OAI.QuarticPowerFree.direct_curve_count_or_hilbert line 138
  9. def OAI.QuarticPowerFree.directSurface line 200
  10. def OAI.QuarticPowerFree.directSurfaceEquiv line 203
  11. theorem OAI.QuarticPowerFree.directSurfaceEquiv_X0 line 207
  12. theorem OAI.QuarticPowerFree.directSurfaceEquiv_X1 line 212
  13. theorem OAI.QuarticPowerFree.directSurfaceEquiv_X2 line 216
  14. theorem OAI.QuarticPowerFree.directSurfaceEquiv_C line 221
  15. theorem OAI.QuarticPowerFree.directSurfaceEquiv_apply line 225
  16. theorem OAI.QuarticPowerFree.directSurface_coeff_relprime line 237
  17. theorem OAI.QuarticPowerFree.directSurface_irreducible line 254
  18. theorem OAI.QuarticPowerFree.coeff_single_eval₂_C_X line 261
  19. theorem OAI.QuarticPowerFree.directSurface_coeff_single line 272
  20. theorem OAI.QuarticPowerFree.directSurface_weightedDegree_lower line 283
  21. theorem OAI.QuarticPowerFree.totalDegree_pos_of_irreducible line 292