OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinates.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Projective.evalAway line 18
  2. lemma OAI.PiExponentSeshadri.Projective.evalAway_val line 22
  3. lemma OAI.PiExponentSeshadri.Projective.evalAway_transition line 25
  4. lemma OAI.PiExponentSeshadri.Projective.evalAway_natural line 40
  5. lemma OAI.PiExponentSeshadri.Projective.evalAway_mk_clear line 51
  6. lemma OAI.PiExponentSeshadri.Projective.evalAway_scale line 60
  7. def OAI.PiExponentSeshadri.Projective.fromUnitCoordinate line 76
  8. lemma OAI.PiExponentSeshadri.Projective.fromUnitCoordinate_mul line 80
  9. lemma OAI.PiExponentSeshadri.Projective.fromUnitCoordinate_natural line 90
  10. lemma OAI.PiExponentSeshadri.Projective.fromUnitCoordinate_scale line 97
  11. lemma OAI.PiExponentSeshadri.Projective.fromUnitCoordinate_preimage line 104
  12. theorem OAI.PiExponentSeshadri.Projective.fromUnitCoordinate_eq line 116
  13. lemma OAI.PiExponentSeshadri.Projective.coordinates_X_mem line 132
  14. def OAI.PiExponentSeshadri.Projective.coordinatesMap line 135
  15. lemma OAI.PiExponentSeshadri.Projective.coordinates_eval_natural line 140
  16. lemma OAI.PiExponentSeshadri.Projective.coordinatesMap_natural line 146
  17. lemma OAI.PiExponentSeshadri.Projective.coordinatesMap_scale line 160
  18. lemma OAI.PiExponentSeshadri.Projective.coordinatesMap_preimage line 186
  19. structure OAI.PiExponentSeshadri.Projective.CoordinateAtlas line 195
  20. def OAI.PiExponentSeshadri.Projective.CoordinateAtlas.localMap line 212
  21. lemma OAI.PiExponentSeshadri.Projective.CoordinateAtlas.compatible line 216
  22. def OAI.PiExponentSeshadri.Projective.CoordinateAtlas.morphism line 229
  23. lemma OAI.PiExponentSeshadri.Projective.CoordinateAtlas.cover_morphism line 233
  24. def OAI.PiExponentSeshadri.Projective.atlasOfFramedSections line 246
  25. def OAI.PiExponentSeshadri.Projective.sectionFrame line 268
  26. lemma OAI.PiExponentSeshadri.Projective.sectionFrame_normalized line 274
  27. def OAI.PiExponentSeshadri.Projective.sectionsMorphism line 279
  28. lemma OAI.PiExponentSeshadri.Projective.sectionsMorphism_local line 295
  29. theorem OAI.PiExponentSeshadri.Projective.sectionsMorphism_preimage line 308
  30. lemma OAI.PiExponentSeshadri.Projective.identityCoordinateOpen line 338
  31. def OAI.PiExponentSeshadri.Projective.sectionFrameOn line 350
  32. lemma OAI.PiExponentSeshadri.Projective.sectionFrameOn_normalized line 353