OAI/RingTheory/Multiplicity/RootProjectiveEuler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ProjectiveRoot.coordinateMul line 15
2. def OAI.Lech.ProjectiveRoot.eulerLeft line 25
3. def OAI.Lech.ProjectiveRoot.eulerRight line 29
4. lemma OAI.Lech.ProjectiveRoot.chartBaseChange_tmul_val line 40
5. lemma OAI.Lech.ProjectiveRoot.chartBaseChange_coordinateMul line 49
6. def OAI.Lech.ProjectiveRoot.chartEulerMiddle line 61
7. lemma OAI.Lech.ProjectiveRoot.intersection_euler_shortExact line 68
8. theorem OAI.Lech.ProjectiveRoot.euler_shortExact line 122
9. lemma OAI.Lech.ProjectiveRoot.coordinateMul_natural line 130