OAI/RingTheory/Multiplicity/ReesRootCech.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.FiniteModuleCech.positiveComplex line 15
2. lemma OAI.Lech.FiniteModuleCech.positiveComplex_d line 21
3. lemma OAI.Lech.FiniteModuleCech.positiveComplex_bounded line 26
4. def OAI.Lech.FiniteModuleCech.Map.positiveComplex line 29
5. abbrev OAI.Lech.ReesRoot.CechSection line 66
6. abbrev OAI.Lech.ReesRoot.cechObj line 69
7. def OAI.Lech.ReesRoot.cechRes line 72
8. lemma OAI.Lech.ReesRoot.cechRes_apply line 82
9. lemma OAI.Lech.ReesRoot.cechRes_self line 88
10. lemma OAI.Lech.ReesRoot.cechRes_comp line 96
11. def OAI.Lech.ReesRoot.cechDiagram line 117
12. def OAI.Lech.ReesRoot.cech line 124
13. lemma OAI.Lech.ReesRoot.cech_bounded line 127