OAI/NumberTheory/PiExponent/Ampleness/ReesPrincipalLift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.BlowupLift.coefficient line 13
  2. lemma OAI.PiExponentSeshadri.BlowupLift.mul_coefficient line 17
  3. lemma OAI.PiExponentSeshadri.BlowupLift.coefficients_span line 23
  4. def OAI.PiExponentSeshadri.ReesGrading.principalToLocalization line 51
  5. lemma OAI.PiExponentSeshadri.ReesGrading.principalToLocalization_base line 55
  6. lemma OAI.PiExponentSeshadri.ReesGrading.principalToLocalization_generator line 60
  7. lemma OAI.PiExponentSeshadri.ReesGrading.principalToLocalization_range line 72
  8. lemma OAI.PiExponentSeshadri.ReesGrading.principalLocalization_injective line 92
  9. def OAI.PiExponentSeshadri.ReesGrading.principalMap line 95
  10. lemma OAI.PiExponentSeshadri.ReesGrading.principalMap_spec line 110
  11. lemma OAI.PiExponentSeshadri.ReesGrading.principalMap_base line 115
  12. lemma OAI.PiExponentSeshadri.ReesGrading.principalMap_generator line 120
  13. lemma OAI.PiExponentSeshadri.ReesGrading.principalMap_irrelevant line 125
  14. def OAI.PiExponentSeshadri.ReesGrading.principalScheme line 143
  15. lemma OAI.PiExponentSeshadri.ReesGrading.principalScheme_projection line 148
  16. lemma OAI.PiExponentSeshadri.ReesGrading.principalScheme_preimage line 173