OAI/AlgebraicGeometry/Seshadri/Blowup/ReesCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.ReesGrading.chartToLocalization line 15
  2. lemma OAI.MaximalSeshadri.ReesGrading.chartToLocalization_mk line 22
  3. lemma OAI.MaximalSeshadri.ReesGrading.chartToLocalization_base line 34
  4. lemma OAI.MaximalSeshadri.ReesGrading.coeff_power_dvd line 39
  5. lemma OAI.MaximalSeshadri.ReesGrading.chartToLocalization_range line 48
  6. lemma OAI.MaximalSeshadri.ReesGrading.localizationMap_injective line 63
  7. def OAI.MaximalSeshadri.ReesGrading.chartLift line 68
  8. lemma OAI.MaximalSeshadri.ReesGrading.chartLift_spec line 84
  9. lemma OAI.MaximalSeshadri.ReesGrading.chartLift_base line 90
  10. lemma OAI.MaximalSeshadri.ReesGrading.base_pow_mul_mk line 103
  11. lemma OAI.MaximalSeshadri.ReesGrading.chartLift_unique line 113
  12. theorem OAI.MaximalSeshadri.ReesGrading.chart_universal line 127
  13. lemma OAI.MaximalSeshadri.ReesGrading.generators_adjoin line 140
  14. lemma OAI.MaximalSeshadri.ReesGrading.generators_adjoin_zero line 154
  15. lemma OAI.MaximalSeshadri.ReesGrading.iSup_generator_basicOpen line 169
  16. def OAI.MaximalSeshadri.ReesGrading.chartCover line 174
  17. lemma OAI.MaximalSeshadri.ReesGrading.chartCover_projection line 186