OAI/NumberTheory/PiExponent/Ampleness/AffineBlowupUniversal.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PiExponentSeshadri.IdealPullback.specIdeal_coordinateline 12 - lemma
OAI.PiExponentSeshadri.ReesGrading.invertible_uniqueline 29 - lemma
OAI.PiExponentSeshadri.ReesGrading.local_liftline 42 - theorem
OAI.PiExponentSeshadri.ReesGrading.affineBlowup_universalline 54