OAI/NumberTheory/PiExponent/Ampleness/GlobalBlowupJetSurjectivity.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponent.BlowupJetSurjectivity.blowupBundleline 14 - theorem
OAI.PiExponent.BlowupJetSurjectivity.eventual_blowup_jetRestriction_surjective_of_section_comparisonline 19