OAI/NumberTheory/PiExponent/Geometry/ProjectivePullbackFrames.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.Geometry.pullbackRestrictFactorNatIso line 11
2. theorem OAI.PiExponentSeshadri.Geometry.exists_restricted_pullback_frame_all_of_factor line 23
3. theorem OAI.PiExponentSeshadri.Geometry.exists_restricted_pullback_frame_all line 69
4. def OAI.PiExponentSeshadri.Geometry.restrictedPullbackFrame line 79
5. lemma OAI.PiExponentSeshadri.Geometry.restrictedPullbackFrame_coefficient line 85