OAI/AlgebraicGeometry/Seshadri/Divisors/CenteredSections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.Projective.scalarEnd_zero line 22
  2. lemma OAI.MaximalSeshadri.Projective.scalarEnd_one line 27
  3. def OAI.MaximalSeshadri.Projective.shiftCoefficients line 31
  4. lemma OAI.MaximalSeshadri.Projective.linearEquation_single line 35
  5. lemma OAI.MaximalSeshadri.Projective.linearEquation_add line 44
  6. lemma OAI.MaximalSeshadri.Projective.linearEquation_shiftCoefficients line 49
  7. def OAI.MaximalSeshadri.Projective.shiftedSections line 54
  8. lemma OAI.MaximalSeshadri.Projective.coefficient_shiftedSections line 58
  9. lemma OAI.MaximalSeshadri.Projective.shiftedSections_none line 71
  10. lemma OAI.MaximalSeshadri.Projective.shiftedSections_preimage line 77
  11. lemma OAI.MaximalSeshadri.Projective.shiftedSections_cover line 90
  12. lemma OAI.MaximalSeshadri.Projective.eval₂_comp_shift line 97
  13. lemma OAI.MaximalSeshadri.Projective.coordinatesMap_comp_shift line 107
  14. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_shift line 120
  15. theorem OAI.MaximalSeshadri.Projective.shiftedSections_closed line 143