OAI/NumberTheory/PiExponent/Ampleness/CurveBlowupImage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.CurveBlowupImage.imageCurve line 15
2. def OAI.PiExponent.CurveBlowupImage.imageMap line 28
3. theorem OAI.PiExponent.CurveBlowupImage.imageMap_comp line 33
4. instance OAI.PiExponent.CurveBlowupImage.imageMap_isProper line 39
5. instance OAI.PiExponent.CurveBlowupImage.imageMap_isDominant line 44
6. theorem OAI.PiExponent.CurveBlowupImage.imageMap_isFinite line 51
7. theorem OAI.PiExponent.CurveBlowupImage.imageMap_restrict_isIso line 59
8. theorem OAI.PiExponent.CurveBlowupImage.imageMap_preimage_nonempty line 67
9. def OAI.PiExponent.CurveBlowupImage.imageFunctionFieldIso line 77
10. theorem OAI.PiExponent.CurveBlowupImage.imageFunctionFieldIso_generic line 87
11. theorem OAI.PiExponent.CurveBlowupImage.blowup_restrict_isIso line 101