OAI/RingTheory/Multiplicity/RootChartUlrich.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ProductSourceCover.powerSection line 14
2. lemma OAI.Lech.RootChartAtlas.globalCoefficientA_homogeneous line 36
3. lemma OAI.Lech.RootChartAtlas.globalCoefficientA_consecutive line 66
4. lemma OAI.Lech.RootChartAtlas.exists_consecutive_section_basis line 78
5. theorem OAI.Lech.ProductSourceCover.exists_powerSection_basis line 95
6. theorem OAI.Lech.ProjectiveRoot.exists_powerSection_basis line 114
7. def OAI.Lech.ProjectiveRoot.powerSectionBasis line 131
8. lemma OAI.Lech.ProjectiveRoot.powerSectionBasis_val line 135