OAI/RingTheory/Multiplicity/ReesUlrichCech.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.FiniteModuleCech.positiveIso line 13
2. abbrev OAI.Lech.ReesRoot.ScalarCechSection line 46
3. abbrev OAI.Lech.ReesRoot.scalarCechObj line 47
4. def OAI.Lech.ReesRoot.scalarCechRes line 49
5. lemma OAI.Lech.ReesRoot.scalarCechRes_apply line 64
6. def OAI.Lech.ReesRoot.scalarCechDiagram line 71
7. def OAI.Lech.ReesRoot.powerScalarDiagram line 101
8. def OAI.Lech.ReesRoot.ulrichCechEquiv line 129
9. lemma OAI.Lech.ReesRoot.ulrichCechEquiv_natural line 141
10. def OAI.Lech.ReesRoot.ulrichCechIso line 157