OAI/RingTheory/Multiplicity/ReesRootGLayer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.ReesRoot.layerAt line 21
2. def OAI.Lech.ReesRoot.layerAtProjection line 25
3. lemma OAI.Lech.ReesRoot.layerAtProjection_f line 28
4. lemma OAI.Lech.ReesRoot.enlarged_first_range line 35
5. lemma OAI.Lech.ReesRoot.enlarged_first_injective line 41
6. lemma OAI.Lech.ReesRoot.layerAt_zero line 46
7. def OAI.Lech.ReesRoot.enlargedLayerShortComplex line 63
8. lemma OAI.Lech.ReesRoot.enlargedLayerShortComplex_exact line 67
9. def OAI.Lech.ReesRoot.exceptionalCechZIso line 91
10. def OAI.Lech.ReesRoot.layerAtRowIso line 101