OAI/NumberTheory/PowerFree/CurveAlternatives.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.algebraic_coordinate_constant line 9
  2. theorem OAI.QuarticPowerFree.curve_coordinate_relation line 21
  3. def OAI.QuarticPowerFree.binaryPolynomialEquiv line 43
  4. theorem OAI.QuarticPowerFree.binaryPolynomialEquiv_natDegree line 47
  5. theorem OAI.QuarticPowerFree.binaryPolynomialEquiv_eval line 53
  6. theorem OAI.QuarticPowerFree.uniquePolynomial_natDegree_le line 70
  7. theorem OAI.QuarticPowerFree.binaryPolynomial_coeff_degree line 80
  8. theorem OAI.QuarticPowerFree.linear_projection_rational line 90
  9. def OAI.QuarticPowerFree.binaryStripExponent line 127
  10. theorem OAI.QuarticPowerFree.binaryStripExponent_injective line 130
  11. theorem OAI.QuarticPowerFree.projection_strip_independent line 140
  12. theorem OAI.QuarticPowerFree.coordinate_power_mem_weighted line 176
  13. theorem OAI.QuarticPowerFree.projection_strip_hilbert line 188
  14. theorem OAI.QuarticPowerFree.projection_curve_hilbert_gain line 215
  15. theorem OAI.QuarticPowerFree.polynomial_of_constant_denominator line 231
  16. theorem OAI.QuarticPowerFree.squarefree_surface_polynomial_coordinate line 244
  17. theorem OAI.QuarticPowerFree.projection_equation_quotient line 262
  18. theorem OAI.QuarticPowerFree.direct_curve_alternative line 276