OAI/NumberTheory/PiExponent/Geometry/ProjectiveFramedSections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Projective.framedSectionsMorphism line 22
  2. lemma OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_local line 26
  3. theorem OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_preimage line 33
  4. theorem OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_over line 47
  5. instance OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_proper line 58
  6. theorem OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_closed line 66
  7. theorem OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_eq line 103
  8. lemma OAI.PiExponentSeshadri.Projective.framedSectionsMorphism_eq_sectionsMorphism line 143
  9. lemma OAI.PiExponentSeshadri.Projective.coefficient_postcomp line 161
  10. theorem OAI.PiExponentSeshadri.Projective.sectionsMorphism_transport line 182