OAI/AlgebraicGeometry/Seshadri/Blowup/PowerContraction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MaximalSeshadri.PlaneBlowup.blowup_power_contractionline 14 - lemma
OAI.MaximalSeshadri.IdealPullback.comap_map_le_of_commSqline 69 - lemma
OAI.MaximalSeshadri.IdealPullback.le_of_openCoverline 77 - lemma
OAI.MaximalSeshadri.IdealPullback.power_contraction_of_openCoverline 95 - theorem
OAI.MaximalSeshadri.PointBlowup.point_power_contractionline 121 - theorem
OAI.MaximalSeshadri.PointBlowup.rational_point_power_contractionline 188