OAI/NumberTheory/PiExponent/Ampleness/ReesUniversalUniqueness.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.ReesGrading.base_pow_mul_mk line 14
  2. lemma OAI.PiExponentSeshadri.ProjBase.basicOpenToSpec_eq line 32
  3. lemma OAI.PiExponentSeshadri.ProjBase.basicOpenToSpec_mem line 40
  4. lemma OAI.PiExponentSeshadri.ProjBase.toSpecZero_mem line 49
  5. lemma OAI.PiExponentSeshadri.ProjBase.toSpecZero_preimage line 62
  6. instance OAI.PiExponentSeshadri.ReesGrading.projection_separated line 75
  7. lemma OAI.PiExponentSeshadri.ReesGrading.projection_mem line 80
  8. lemma OAI.PiExponentSeshadri.ReesGrading.projection_preimage line 86
  9. lemma OAI.PiExponentSeshadri.ReesGrading.base_generator_comm line 92
  10. lemma OAI.PiExponentSeshadri.ReesGrading.projection_preimage_le_chart line 99
  11. lemma OAI.PiExponentSeshadri.ReesGrading.chartHom_ext line 112
  12. lemma OAI.PiExponentSeshadri.ReesGrading.chart_scheme_ext line 126
  13. lemma OAI.PiExponentSeshadri.ReesGrading.ext_of_unit_generator line 138
  14. lemma OAI.PiExponentSeshadri.ReesGrading.ext_on_generator_open line 180
  15. lemma OAI.PiExponentSeshadri.ReesGrading.ext_of_unit_ideal line 193
  16. lemma OAI.PiExponentSeshadri.ReesGrading.principal_basicOpen_unit_ideal line 205
  17. lemma OAI.PiExponentSeshadri.ReesGrading.principal_unique line 215