OAI/NumberTheory/PowerFree/AffineHilbert.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuarticPowerFree.independent_one_transcendental line 12
  2. lemma OAI.QuarticPowerFree.affine_left_dichotomy line 21
  3. theorem OAI.QuarticPowerFree.norm_surface_left_basis line 62
  4. lemma OAI.QuarticPowerFree.conjugate_affine_slope_ne_zero line 91
  5. lemma OAI.QuarticPowerFree.pairAExponent_sum_low line 115
  6. def OAI.QuarticPowerFree.affineExponent line 129
  7. lemma OAI.QuarticPowerFree.affineExponent_injective line 132
  8. lemma OAI.QuarticPowerFree.exists_affineExponent line 153
  9. theorem OAI.QuarticPowerFree.pairCone_low_affine_degree_injective line 170
  10. theorem OAI.QuarticPowerFree.rootPair_actual_hilbert_uniform_affine line 222
  11. lemma OAI.QuarticPowerFree.affine_pair_projection_bounded line 281
  12. theorem OAI.QuarticPowerFree.norm_ambient_hilbert_uniform_affine_pair line 322