OAI/NumberTheory/PiExponent/Ampleness/AdmissibleBlowupMargin.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.PiExponent.AdmissibleBlowupMargin.AffineCurveDegreeDataline 14 - theorem
OAI.PiExponent.AdmissibleBlowupMargin.uniform_margin_of_affine_curve_dataline 29 - theorem
OAI.PiExponent.AdmissibleBlowupMargin.exists_positive_uniform_margin_of_affine_curve_dataline 61