OAI/RingTheory/Multiplicity/RootCoefficientEuler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ProductSourceCover.rootCoordinate line 15
2. lemma OAI.Lech.ProductSourceCover.coordinate_ringSections line 18
3. lemma OAI.Lech.ProductSourceCover.rootCoordinate_mem line 35
4. def OAI.Lech.ProductSourceCover.coordinateMul line 46
5. def OAI.Lech.ProductSourceCover.eulerLeft line 57
6. def OAI.Lech.ProductSourceCover.eulerRight line 61
7. lemma OAI.Lech.RootChartAtlas.globalSection_coordinateMul line 79
8. lemma OAI.Lech.RootChartAtlas.section_euler_shortExact line 88
9. theorem OAI.Lech.ProductSourceCover.euler_shortExact line 122