OAI/RingTheory/Multiplicity/ReesRootThickeningEuler.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.ReesRoot.thickeningZ line 14
2. abbrev OAI.Lech.ReesRoot.firstZ line 15
3. def OAI.Lech.ReesRoot.firstZIso line 17
4. lemma OAI.Lech.ReesRoot.cechZ_bounded line 19
5. lemma OAI.Lech.ReesRoot.thickeningZ_bounded line 24
6. lemma OAI.Lech.ReesRoot.thickeningZ_homology_bounded line 28
7. lemma OAI.Lech.ReesRoot.firstZ_homology_bounded line 32
8. lemma OAI.Lech.ReesRoot.thickeningZ_zero line 37
9. def OAI.Lech.ReesRoot.thickeningShortComplex line 47
10. lemma OAI.Lech.ReesRoot.thickeningShortComplex_exact line 51
11. lemma OAI.Lech.ReesRoot.firstZ_finite line 60
12. lemma OAI.Lech.ReesRoot.thickeningZ_finite line 65
13. lemma OAI.Lech.ReesRoot.firstZ_euler line 74
14. lemma OAI.Lech.ReesRoot.raise_raise line 80
15. theorem OAI.Lech.ReesRoot.thickeningZ_euler line 87