OAI/NumberTheory/PowerFree/GenericCuts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.genericPoint line 16
  2. theorem OAI.QuarticPowerFree.aeval_genericPoint line 21
  3. theorem OAI.QuarticPowerFree.aeval_genericPoint_eq_zero_iff line 30
  4. theorem OAI.QuarticPowerFree.aeval_jacobian_det line 39
  5. theorem OAI.QuarticPowerFree.bounded_patch_or_cut line 46
  6. lemma OAI.QuarticPowerFree.monomial_exponent_le_order line 98
  7. theorem OAI.QuarticPowerFree.eval_abs_le_height_degree line 105
  8. theorem OAI.QuarticPowerFree.pderiv_coeff_abs_le line 135
  9. theorem OAI.QuarticPowerFree.pderiv_degree_le_sub_one line 154
  10. theorem OAI.QuarticPowerFree.jacobian_minor_degree line 162
  11. theorem OAI.QuarticPowerFree.eval_jacobian_minor_abs_le line 181
  12. theorem OAI.QuarticPowerFree.coordinate_transcendence_basis line 201
  13. theorem OAI.QuarticPowerFree.hilbert_natDegree_eq_trdeg line 232
  14. theorem OAI.QuarticPowerFree.proper_cut_hilbert_inequality line 265
  15. theorem OAI.QuarticPowerFree.coeff_taylor_high line 322
  16. theorem OAI.QuarticPowerFree.hilbert_difference_degree line 329
  17. theorem OAI.QuarticPowerFree.hilbert_difference_coeff line 335
  18. theorem OAI.QuarticPowerFree.proper_cut_hilbert_polynomial line 349