OAI/NumberTheory/PowerFree/DegreeBudgets.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.minimal_prime_separators line 16
  2. theorem OAI.QuarticPowerFree.component_hilbert_sum_le_shift line 42
  3. theorem OAI.QuarticPowerFree.component_hilbert_coeff_sum_le line 109
  4. theorem OAI.QuarticPowerFree.polynomial_eq_of_eventually_nat_eval_eq line 143
  5. def OAI.QuarticPowerFree.coordinateHilbert line 151
  6. def OAI.QuarticPowerFree.affineDimension line 155
  7. def OAI.QuarticPowerFree.affineDegree line 158
  8. theorem OAI.QuarticPowerFree.coordinateHilbert_eventually line 162
  9. theorem OAI.QuarticPowerFree.one_le_affineDegree line 169
  10. theorem OAI.QuarticPowerFree.proper_cut_component_dimension line 183
  11. theorem OAI.QuarticPowerFree.proper_cut_sum_affineDegree_le line 191
  12. theorem OAI.QuarticPowerFree.proper_cut_component_card_le line 221
  13. def OAI.QuarticPowerFree.DeterminedInDegree line 237
  14. theorem OAI.QuarticPowerFree.totalDegree_map_ringEquiv line 242
  15. theorem OAI.QuarticPowerFree.eval_integer_point_map line 248
  16. theorem OAI.QuarticPowerFree.determined_equations_invariant line 258
  17. theorem OAI.QuarticPowerFree.bounded_cut_or_determined line 266