OAI/NumberTheory/PiExponent/Approximation/FrameSections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Frames.scalarEnd line 16
  2. lemma OAI.PiExponentSeshadri.Frames.endValue_scalarEnd line 32
  3. lemma OAI.PiExponentSeshadri.Frames.endValue_injective line 36
  4. lemma OAI.PiExponentSeshadri.Frames.end_isIso_iff line 44
  5. lemma OAI.PiExponentSeshadri.Frames.coefficient_isUnit_iff line 60
  6. def OAI.PiExponentSeshadri.Frames.moduleSectionsTopEquiv line 73
  7. def OAI.PiExponentSeshadri.Frames.moduleSectionEquiv line 91
  8. lemma OAI.PiExponentSeshadri.Frames.moduleSectionEquiv_apply line 94
  9. def OAI.PiExponentSeshadri.Frames.openSectionEquiv line 97
  10. lemma OAI.PiExponentSeshadri.Frames.section_value_natural line 106
  11. lemma OAI.PiExponentSeshadri.Frames.openSectionEquiv_restrict line 113
  12. lemma OAI.PiExponentSeshadri.Frames.moduleSectionEquiv_scalar line 126
  13. lemma OAI.PiExponentSeshadri.Frames.openSectionEquiv_scalar line 134
  14. lemma OAI.PiExponentSeshadri.Frames.openSectionEquiv_restrict_value line 145
  15. lemma OAI.PiExponentSeshadri.Frames.image_section_extension line 157