OAI/NumberTheory/PowerFree/ThreePoles.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.linearIndependent_of_fin_top_blocks line 11
  2. def OAI.QuarticPowerFree.threePoleClearing line 39
  3. def OAI.QuarticPowerFree.threePolePolynomial line 43
  4. lemma OAI.QuarticPowerFree.threePolePolynomial_degree line 51
  5. lemma OAI.QuarticPowerFree.threePolePolynomial_coeff line 65
  6. theorem OAI.QuarticPowerFree.threePole_polynomials_independent line 107
  7. def OAI.QuarticPowerFree.bivarEvaluation line 134
  8. lemma OAI.QuarticPowerFree.bivarEvaluation_C line 138
  9. lemma OAI.QuarticPowerFree.bivarEvaluation_X line 142
  10. theorem OAI.QuarticPowerFree.bivarEvaluation_injective line 146
  11. theorem OAI.QuarticPowerFree.threePole_evaluations_independent line 173
  12. lemma OAI.QuarticPowerFree.square_relation_power line 184
  13. lemma OAI.QuarticPowerFree.threePole_base_identity line 191
  14. lemma OAI.QuarticPowerFree.threePole_extra_identity line 202
  15. def OAI.QuarticPowerFree.threePoleFunction line 219
  16. lemma OAI.QuarticPowerFree.threePole_evaluation_identity line 225
  17. theorem OAI.QuarticPowerFree.threePole_functions_independent line 254