OAI/RingTheory/Multiplicity/ReesRootEuler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ReesRoot.coordinateMul line 37
2. def OAI.Lech.ReesRoot.eulerLeft line 41
3. def OAI.Lech.ReesRoot.eulerRight line 45
4. lemma OAI.Lech.ReesRoot.eulerLeft_baseChange line 51
5. lemma OAI.Lech.ReesRoot.eulerRight_baseChange line 68
6. lemma OAI.Lech.ReesRoot.euler_baseChange_shortExact line 85
7. lemma OAI.Lech.ReesRoot.euler_shortExact line 96
8. lemma OAI.Lech.ReesRoot.coordinateMul_natural line 119
9. def OAI.Lech.ReesRoot.coordinateCechHom line 131
10. lemma OAI.Lech.ReesRoot.coordinateCechHom_natural line 140
11. def OAI.Lech.ReesRoot.coordinateCechMap line 157