OAI/NumberTheory/PiExponent/Approximation/IntegralLineSections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Geometry.trivialModule_restriction_injective line 14
  2. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.restriction_injective line 29
  3. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.section_restriction_injective line 63
  4. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.noZeroSMulDivisors line 93
  5. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.mono_section line 138
  6. lemma OAI.PiExponentSeshadri.Frames.coefficient_injective line 176
  7. lemma OAI.PiExponentSeshadri.Frames.coefficient_zero line 181
  8. lemma OAI.PiExponentSeshadri.Frames.restrictSection_zero line 185
  9. lemma OAI.PiExponentSeshadri.Geometry.LineBundle.restrict_sections_injective line 195
  10. lemma OAI.PiExponentSeshadri.Geometry.LineBundle.restricted_coefficient_injective line 209
  11. lemma OAI.PiExponentSeshadri.Geometry.LineBundle.isoOpen_ne_bot line 220
  12. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.sectionOpen_nonempty line 239