OAI/NumberTheory/PowerFree/NormHilbert.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.pairSplitFirst line 12
  2. theorem OAI.QuarticPowerFree.pairSplitFirst_injective line 15
  3. theorem OAI.QuarticPowerFree.pairSplitFirst_weight line 24
  4. theorem OAI.QuarticPowerFree.ambientPairTuples_card_full line 31
  5. theorem OAI.QuarticPowerFree.ambientPairTuples_hilbert_error line 71
  6. theorem OAI.QuarticPowerFree.norm_full_projection_independent line 103
  7. theorem OAI.QuarticPowerFree.rootPair_evaluation_injective line 132
  8. theorem OAI.QuarticPowerFree.pairCone_full_finrank line 164
  9. theorem OAI.QuarticPowerFree.norm_full_hilbert_uniform line 191
  10. theorem OAI.QuarticPowerFree.uniform_real_hilbert_floor line 244
  11. theorem OAI.QuarticPowerFree.norm_full_real_hilbert_uniform line 295