OAI/RingTheory/Multiplicity/ExceptionalRootCohomology.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ProjectiveRoot.cech_empty_zero line 16
2. abbrev OAI.Lech.ProjectiveRoot.reducedPositive line 21
3. def OAI.Lech.ProjectiveRoot.reducedPositiveHomologyIso line 24
4. lemma OAI.Lech.ProjectiveRoot.reducedPositive_length_eq line 31
5. lemma OAI.Lech.ProjectiveRoot.reducedPositive_length line 38
6. lemma OAI.Lech.ProjectiveRoot.reducedPositive_length_zero line 43
7. lemma OAI.Lech.ProjectiveRoot.reducedPositive_length_finite line 47
8. abbrev OAI.Lech.ReesRoot.exceptionalCech line 63
9. lemma OAI.Lech.ReesRoot.exceptional_length_eq line 67
10. theorem OAI.Lech.ReesRoot.exceptional_length line 77
11. lemma OAI.Lech.ReesRoot.exceptional_length_zero line 84
12. lemma OAI.Lech.ReesRoot.exceptional_length_finite line 90
13. lemma OAI.Lech.ReesRoot.exceptional_torsion line 96
14. theorem OAI.Lech.ReesRoot.exceptional_root_euler line 101