OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateFiniteSections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Projective.isoPreimageSectionRingEquiv line 15
  2. abbrev OAI.PiExponentSeshadri.Projective.schemeFreeOpen line 20

    Distinct definitions of this name: OAI/NumberTheory/PiExponent/Cohomology/ProjectiveFramedCech.lean:21 (different declaration text), OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateSections.lean:25 (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.

  3. def OAI.PiExponentSeshadri.Projective.coordinateFiniteOpen line 26
  4. lemma OAI.PiExponentSeshadri.Projective.coordinateFiniteOpen_eq_preimage line 33
  5. def OAI.PiExponentSeshadri.Projective.coordinateFiniteRingEquiv line 47
  6. def OAI.PiExponentSeshadri.Projective.coordinatePowerOverlap line 56
  7. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerOverlap_injective line 64
  8. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerOverlap_regular line 68
  9. lemma OAI.PiExponentSeshadri.Projective.coordinatePowerOverlap_surjective_regular line 74