OAI/NumberTheory/PiExponent/Jets/CompactJetIdeal.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponent.CompactJetIdeal.extendline 14 - theorem
OAI.PiExponent.CompactJetIdeal.restrict_extendline 16 - theorem
OAI.PiExponent.CompactJetIdeal.section_isClosedImmersionline 27 - theorem
OAI.PiExponent.CompactJetIdeal.image_support_isClosedline 32 - theorem
OAI.PiExponent.CompactJetIdeal.support_extendline 49 - theorem
OAI.PiExponent.CompactJetIdeal.restrict_eq_top_of_disjointline 59 - abbrev
OAI.PiExponent.CompactJetIdeal.affineBlowupline 67