OAI/NumberTheory/PiExponent/Ampleness/ReesLocalizedIntersections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.ReesLocalizedIntersections.coefficientProduct line 15
  2. theorem OAI.PiExponent.ReesLocalizedIntersections.evaluation_presentation_product line 18
  3. abbrev OAI.PiExponent.ReesLocalizedIntersections.LocalizationModule line 22
  4. def OAI.PiExponent.ReesLocalizedIntersections.localizationEvaluation line 27
  5. theorem OAI.PiExponent.ReesLocalizedIntersections.localizationEvaluation_fraction line 39
  6. theorem OAI.PiExponent.ReesLocalizedIntersections.localizationEvaluation_smul line 55
  7. def OAI.PiExponent.ReesLocalizedIntersections.coefficientRestriction line 64
  8. theorem OAI.PiExponent.ReesLocalizedIntersections.coefficientRestriction_algebraMap line 72
  9. theorem OAI.PiExponent.ReesLocalizedIntersections.localizationEvaluation_restriction line 78
  10. abbrev OAI.PiExponent.ReesLocalizedIntersections.Piece line 117
  11. def OAI.PiExponent.ReesLocalizedIntersections.pieceEvaluation line 123
  12. theorem OAI.PiExponent.ReesLocalizedIntersections.pieceEvaluation_restriction line 129
  13. theorem OAI.PiExponent.ReesLocalizedIntersections.pieceEvaluation_injective line 140