OAI/NumberTheory/PowerFree/QuarticPairs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.pairConeB line 10
  2. def OAI.QuarticPowerFree.pairABExponent line 15
  3. lemma OAI.QuarticPowerFree.pairConeBasis_map line 20
  4. def OAI.QuarticPowerFree.pairConePolynomial line 38
  5. lemma OAI.QuarticPowerFree.pairConePolynomial_eval line 44
  6. lemma OAI.QuarticPowerFree.pairConePolynomial_weight line 65
  7. def OAI.QuarticPowerFree.leftExponent line 98
  8. theorem OAI.QuarticPowerFree.quartic_exponent_classification line 102
  9. lemma OAI.QuarticPowerFree.monomial_left_only line 153
  10. theorem OAI.QuarticPowerFree.quartic_low_polynomial line 165
  11. theorem OAI.QuarticPowerFree.pairCone_small_relation line 212
  12. theorem OAI.QuarticPowerFree.paired_denominator_ne_zero line 258
  13. theorem OAI.QuarticPowerFree.quartic_paired_rational_identity line 273
  14. theorem OAI.QuarticPowerFree.quartic_paired_field line 284