OAI/NumberTheory/PowerFree/WeightedFunctions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.weightedFunctions_mono line 11
  2. theorem OAI.QuarticPowerFree.weightedFunctions_one line 16
  3. theorem OAI.QuarticPowerFree.weightedFunctions_mul line 23
  4. theorem OAI.QuarticPowerFree.weightedFunctions_pow line 48
  5. theorem OAI.QuarticPowerFree.weightedFunctions_coordinate line 57
  6. theorem OAI.QuarticPowerFree.polynomial_curve_strip line 65
  7. theorem OAI.QuarticPowerFree.polynomial_curve_hilbert_gain line 94
  8. theorem OAI.QuarticPowerFree.rational_selected_count_general line 125
  9. theorem OAI.QuarticPowerFree.bounded_polynomial_of_constant_denominator line 159
  10. theorem OAI.QuarticPowerFree.curve_polynomial_left_gain line 173
  11. theorem OAI.QuarticPowerFree.norm_curve_polynomial_reduction line 189
  12. theorem OAI.QuarticPowerFree.integer_conjugate_form_injective line 254
  13. def OAI.QuarticPowerFree.conjugateLinePolynomial line 267
  14. theorem OAI.QuarticPowerFree.conjugateLinePolynomial_degree line 271
  15. theorem OAI.QuarticPowerFree.conjugateLinePolynomial_slope_ne_zero line 276
  16. theorem OAI.QuarticPowerFree.curve_polynomial_substitution line 292