OAI/NumberTheory/PowerFree/EmbeddingCharts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.QuarticPowerFree.IntegralEmbeddingChart line 11
  2. def OAI.QuarticPowerFree.integralEmbeddingChart line 18
  3. def OAI.QuarticPowerFree.IntegralEmbeddingChart.A line 36
  4. def OAI.QuarticPowerFree.IntegralEmbeddingChart.coord line 40
  5. theorem OAI.QuarticPowerFree.IntegralEmbeddingChart.embedding line 43
  6. theorem OAI.QuarticPowerFree.IntegralEmbeddingChart.inverse_coordinates line 51
  7. theorem OAI.QuarticPowerFree.IntegralEmbeddingChart.coordinates_bound line 56
  8. theorem OAI.QuarticPowerFree.coordinateLinearForm_inverse line 83
  9. theorem OAI.QuarticPowerFree.coordinateLinearForm_mem_adjoin line 96
  10. theorem OAI.QuarticPowerFree.coordinateLinearForm_totalDegree line 103
  11. theorem OAI.QuarticPowerFree.coordinateLinearForm_weightedSpace line 109
  12. def OAI.QuarticPowerFree.normBoxWeight line 119
  13. def OAI.QuarticPowerFree.normBoxNatWeight line 120
  14. theorem OAI.QuarticPowerFree.normBoxWeight_pos line 122
  15. theorem OAI.QuarticPowerFree.normBoxWeight_le line 124
  16. theorem OAI.QuarticPowerFree.normBoxNatWeight_ne line 126
  17. theorem OAI.QuarticPowerFree.normBoxWeight_scale line 128
  18. theorem OAI.QuarticPowerFree.pairedLinearForms_generate line 131
  19. theorem OAI.QuarticPowerFree.arithmeticModel_distinct line 159
  20. def OAI.QuarticPowerFree.normBoxOfChart line 170
  21. def OAI.QuarticPowerFree.normIntegralPoint line 198
  22. theorem OAI.QuarticPowerFree.normIntegralPoint_left line 202
  23. theorem OAI.QuarticPowerFree.normIntegralPoint_right line 210
  24. theorem OAI.QuarticPowerFree.normIntegralPoint_equation line 219
  25. theorem OAI.QuarticPowerFree.selected_prime_count line 256
  26. theorem OAI.QuarticPowerFree.norm_left_fibre_count line 293