OAI/RingTheory/Multiplicity/RootOverlap.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.ProjectiveRoot.product line 18
  2. lemma OAI.Lech.ProjectiveRoot.product_homogeneous line 20
  3. abbrev OAI.Lech.ProjectiveRoot.Ring line 25
  4. def OAI.Lech.ProjectiveRoot.coefficientEvaluation line 29
  5. lemma OAI.Lech.ProjectiveRoot.coefficientEvaluation_X line 31
  6. lemma OAI.Lech.ProjectiveRoot.coefficientEvaluation_product line 34
  7. lemma OAI.Lech.ProjectiveRoot.coefficientEvaluation_unit line 38
  8. def OAI.Lech.ProjectiveRoot.scalarAt line 44
  9. def OAI.Lech.ProjectiveRoot.scalarMap line 59
  10. lemma OAI.Lech.ProjectiveRoot.coefficientEvaluation_X_unit line 62
  11. lemma OAI.Lech.ProjectiveRoot.product_eq line 69
  12. def OAI.Lech.ProjectiveRoot.chartMap line 73
  13. def OAI.Lech.ProjectiveRoot.coefficientMap line 76
  14. lemma OAI.Lech.ProjectiveRoot.scalarMap_chart line 79
  15. lemma OAI.Lech.ProjectiveRoot.scalarAt_equiv line 84
  16. lemma OAI.Lech.ProjectiveRoot.scalarMap_coefficient line 109
  17. def OAI.Lech.ProjectiveRoot.chartAlgebra line 114
  18. def OAI.Lech.ProjectiveRoot.coefficientAlgebra line 117
  19. lemma OAI.Lech.ProjectiveRoot.isLocalization line 122
  20. lemma OAI.Lech.ProjectiveRoot.scalar_mem line 146
  21. instance OAI.Lech.ProjectiveRoot.ambientAlgebra line 171
  22. instance OAI.Lech.ProjectiveRoot.ambientTower line 173
  23. def OAI.Lech.ProjectiveRoot.Sections line 178
  24. def OAI.Lech.ProjectiveRoot.overlapEquiv line 212
  25. def OAI.Lech.ProjectiveRoot.chartRestriction line 222
  26. instance OAI.Lech.ProjectiveRoot.chartRestriction_localized line 226
  27. def OAI.Lech.ProjectiveRoot.chartBaseChange line 233
  28. lemma OAI.Lech.ProjectiveRoot.chartBaseChange_one line 238
  29. theorem OAI.Lech.ProjectiveRoot.Sections_properties line 246