OAI/NumberTheory/PowerFree/RootPairHilbert.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.norm_projection_bounded line 10
  2. def OAI.QuarticPowerFree.rootPairEvaluation line 60
  3. theorem OAI.QuarticPowerFree.rootPairEvaluation_left line 69
  4. theorem OAI.QuarticPowerFree.rootPairEvaluation_right line 76
  5. theorem OAI.QuarticPowerFree.rootPairEvaluation_number line 83
  6. theorem OAI.QuarticPowerFree.rootPairEvaluation_projection line 90
  7. theorem OAI.QuarticPowerFree.rootPairEvaluation_comp_kernel line 106
  8. theorem OAI.QuarticPowerFree.rootPair_actual_hilbert_uniform_allFields line 127
  9. theorem OAI.QuarticPowerFree.pairCone_homogeneous_image_le line 187
  10. theorem OAI.QuarticPowerFree.rootPair_actual_hilbert_le line 230
  11. theorem OAI.QuarticPowerFree.norm_ambient_hilbert_uniform line 263