OAI/NumberTheory/PowerFree/RationalCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.norm_real_hilbert_uniform line 12
  2. theorem OAI.QuarticPowerFree.curve_parameter_injective line 58
  3. theorem OAI.QuarticPowerFree.curve_input_degree_lower_bound line 72
  4. theorem OAI.QuarticPowerFree.affine_factor_eq line 98
  5. theorem OAI.QuarticPowerFree.curve_polynomial_degrees line 104
  6. theorem OAI.QuarticPowerFree.polynomial_linearIndependent_of_degrees line 140
  7. theorem OAI.QuarticPowerFree.curve_polynomial_families_independent line 166
  8. theorem OAI.QuarticPowerFree.projection_strip_hilbert_weighted line 196
  9. theorem OAI.QuarticPowerFree.projection_curve_hilbert_weighted line 221
  10. theorem OAI.QuarticPowerFree.curve_coordinate_rationalization line 243
  11. theorem OAI.QuarticPowerFree.rational_graph_denominator_ne_zero line 268
  12. theorem OAI.QuarticPowerFree.rational_coordinates_injOn line 278