OAI/RingTheory/Multiplicity/RootFibreCech.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ReesRoot.unitCech line 40
2. lemma OAI.Lech.ReesRoot.unitCech_natural line 45
3. def OAI.Lech.ReesRoot.unitCechMap line 66
4. abbrev OAI.Lech.ReesRoot.rootReductionDiagram line 70
5. abbrev OAI.Lech.ReesRoot.exceptionalDiagram line 71
6. def OAI.Lech.ReesRoot.fibreCechMap line 73
7. lemma OAI.Lech.ReesRoot.fibreCechMap_isoModSerre line 83
8. theorem OAI.Lech.ReesRoot.fibreCech_homology line 101
9. lemma OAI.Lech.ReesRoot.fibreCech_cardinality_homology line 108