OAI/NumberTheory/PiExponent/Ampleness/GlobalBlowupJetSurjectivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.BlowupJetSurjectivity.blowupBundle line 14
  2. theorem OAI.PiExponent.BlowupJetSurjectivity.eventual_blowup_jetRestriction_surjective_of_section_comparison line 19