OAI/NumberTheory/PiExponent/Geometry/ProjectiveChartSections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.ProjectiveChartSections.schemeFreeOpen line 14

    Distinct definitions of this name: OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateScalars.lean:13 (same statement text; different proof or body). Qualify references as OAI.PiExponentSeshadri.ProjectiveChartSections.schemeFreeOpen@path.

  2. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedSectionsEquiv line 19
  3. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedCoefficientsEquiv line 32
  4. def OAI.PiExponentSeshadri.ProjectiveChartSections.freeOpenAddEquiv line 36
  5. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedHomCoefficientsEquiv line 40
  6. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedHomRingEquiv line 44
  7. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentVertex line 53
  8. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentVertex_regular line 58
  9. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentVertex_injective line 64
  10. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentVertex_surjective_regular line 69
  11. def OAI.PiExponentSeshadri.ProjectiveChartSections.powerHomRingEquiv line 80
  12. def OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentOverlap line 85
  13. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentOverlap_injective line 91
  14. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentOverlap_regular line 97
  15. theorem OAI.PiExponentSeshadri.ProjectiveChartSections.framedLaurentOverlap_surjective_regular line 105