OAI/NumberTheory/PowerFree/BoundedLifts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.basis_homogeneous_lift_at_degree line 10
  2. theorem OAI.QuarticPowerFree.minimal_homogeneous_lift_bounded line 33
  3. theorem OAI.QuarticPowerFree.pairCone_bounded_lift line 77
  4. theorem OAI.QuarticPowerFree.pairCone_cut_hilbert_uniform line 108
  5. theorem OAI.QuarticPowerFree.pairAffine_cut_hilbert_uniform line 134
  6. theorem OAI.QuarticPowerFree.pairAffine_bounded_hilbert_uniform line 155
  7. def OAI.QuarticPowerFree.pairAExponent line 197
  8. lemma OAI.QuarticPowerFree.pair_b_exponents_zero line 200
  9. lemma OAI.QuarticPowerFree.pairAExponent_injective_low line 214
  10. def OAI.QuarticPowerFree.pairConeA line 237
  11. lemma OAI.QuarticPowerFree.monomial_eq_univ_prod line 242
  12. lemma OAI.QuarticPowerFree.pairConeBasis_map_low line 249
  13. theorem OAI.QuarticPowerFree.pairCone_low_degree_injective line 270
  14. theorem OAI.QuarticPowerFree.pairCone_independent_lift line 315