OAI/NumberTheory/PowerFree/TwoPoles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuarticPowerFree.fin_sum_nat_cast line 10
  2. theorem OAI.QuarticPowerFree.pole_family_count_lower line 16
  3. lemma OAI.QuarticPowerFree.weightedFunctions_algebraMap line 67
  4. lemma OAI.QuarticPowerFree.threePoleFunction_weighted line 75
  5. theorem OAI.QuarticPowerFree.threePole_hilbert_lower line 102
  6. lemma OAI.QuarticPowerFree.coeff_linear_power line 167
  7. def OAI.QuarticPowerFree.twoPolePolynomial line 174
  8. lemma OAI.QuarticPowerFree.twoPolePolynomial_degree line 184
  9. lemma OAI.QuarticPowerFree.twoPolePolynomial_coeff line 206
  10. theorem OAI.QuarticPowerFree.twoPole_polynomials_independent line 229
  11. def OAI.QuarticPowerFree.twoPoleFunction line 254
  12. lemma OAI.QuarticPowerFree.twoPole_extra_right_identity line 261
  13. lemma OAI.QuarticPowerFree.twoPole_evaluation_identity line 274
  14. theorem OAI.QuarticPowerFree.twoPole_functions_independent line 307