OAI/NumberTheory/PiExponent/LocalAlgebra/IdealPowerFiltration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PiExponentSeshadri.IdealModule.closedInclusion_mono line 14
2. lemma OAI.PiExponentSeshadri.IdealModule.closedInclusion_structureMap_eq_zero line 17
3. def OAI.PiExponentSeshadri.IdealModule.closedMap line 30
4. lemma OAI.PiExponentSeshadri.IdealModule.closedMap_inclusion line 34
5. instance OAI.PiExponentSeshadri.IdealModule.closedMap_mono line 37
6. lemma OAI.PiExponentSeshadri.IdealModule.closedMap_refl line 41
7. lemma OAI.PiExponentSeshadri.IdealModule.closedMap_comp line 45
8. def OAI.PiExponentSeshadri.IdealModule.powerMap line 50
9. instance OAI.PiExponentSeshadri.IdealModule.powerMap_mono line 53
10. def OAI.PiExponentSeshadri.IdealModule.powerLayer line 56
11. def OAI.PiExponentSeshadri.IdealModule.powerSequence line 58
12. theorem OAI.PiExponentSeshadri.IdealModule.powerSequence_shortExact line 61
13. theorem OAI.PiExponentSeshadri.IdealModule.closedModule_bot_isZero line 66
14. theorem OAI.PiExponentSeshadri.IdealModule.closedModule_isFinitePresentation line 76
15. theorem OAI.PiExponentSeshadri.IdealModule.powerLayer_isFinitePresentation line 87
16. theorem OAI.PiExponentSeshadri.IdealModule.powerModule_eventually_isZero line 96