OAI/RingTheory/Multiplicity/ReesRootBundle.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.HomogeneousEval.awayMap_algebraMap line 13
2. lemma OAI.Lech.ProjectiveRoot.ringRestriction_algebraMap line 26
3. lemma OAI.Lech.ReesRoot.gradedMap_smul line 39
4. def OAI.Lech.ReesRoot.mapAlg line 43
5. def OAI.Lech.ReesRoot.restrictionAlg line 52
6. instance OAI.Lech.ReesRoot.projectiveAlgebra line 57
7. instance OAI.Lech.ReesRoot.projectiveTower line 59
8. abbrev OAI.Lech.ReesRoot.Sections line 64
9. def OAI.Lech.ReesRoot.coefficientRestriction line 93
10. def OAI.Lech.ReesRoot.sectionsRestrictionSemi line 102
11. def OAI.Lech.ReesRoot.sectionsRestriction line 108
12. lemma OAI.Lech.ReesRoot.sectionsRestriction_tmul line 124
13. lemma OAI.Lech.ReesRoot.sectionsRestriction_self line 129
14. lemma OAI.Lech.ReesRoot.sectionsRestriction_comp line 135
15. theorem OAI.Lech.ReesRoot.sections_properties line 145