OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateSections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Projective.schemeIsoGammaEquiv line 17
  2. lemma OAI.PiExponentSeshadri.Projective.schemeIsoGammaEquiv_symm_apply line 21
  3. abbrev OAI.PiExponentSeshadri.Projective.schemeFreeOpen line 25

    Distinct definitions of this name: OAI/NumberTheory/PiExponent/Cohomology/ProjectiveFramedCech.lean:21 (different declaration text), OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateFiniteSections.lean:20 (same statement text; different proof or body), OAI/NumberTheory/PiExponent/Geometry/ProjectiveNegativeScalars.lean:13 (same statement text; different proof or body). Qualify references as OAI.PiExponentSeshadri.Projective.schemeFreeOpen@path.

  4. lemma OAI.PiExponentSeshadri.Projective.sectionOpen_eq_coordinate_preimage line 34
  5. def OAI.PiExponentSeshadri.Projective.coordinateSectionChartIso line 39
  6. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionChartIso_hom_away line 45
  7. def OAI.PiExponentSeshadri.Projective.coordinateSectionRingEquiv line 53
  8. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionRingEquiv_coordinate line 59
  9. lemma OAI.PiExponentSeshadri.Projective.coordinateSectionRingEquiv_power_coordinate line 82
  10. def OAI.PiExponentSeshadri.Projective.coordinatePowerVertex line 93
  11. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerVertex_regular line 100
  12. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerVertex_injective line 105
  13. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerVertex_surjective_regular line 109