OAI/RingTheory/Multiplicity/ReesRootLayers.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.LocalPrincipal.smul_top_eq_range line 15
2. lemma OAI.Lech.ReesRoot.inclusion_range line 64
3. abbrev OAI.Lech.ReesRoot.ExceptionalSections line 87
4. def OAI.Lech.ReesRoot.layerEquiv line 91
5. def OAI.Lech.ReesRoot.raise line 98
6. lemma OAI.Lech.ReesRoot.raise_apply line 102
7. def OAI.Lech.ReesRoot.inclusionIter line 109
8. lemma OAI.Lech.ReesRoot.inclusionIter_injective line 115
9. lemma OAI.Lech.ReesRoot.inclusionIter_range line 123
10. lemma OAI.Lech.ReesRoot.inclusionIter_restriction line 136
11. def OAI.Lech.ReesRoot.thickeningEquiv line 151