OAI/NumberTheory/PiExponent/LocalAlgebra/PresentedIdealIso.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.PresentedIdealIso.imageIdealSheaf_eq_comap line 15
2. theorem OAI.PiExponent.PresentedIdealIso.presented_range_eq line 37
3. theorem OAI.PiExponent.PresentedIdealIso.inclusion_structureMap_zero line 48
4. def OAI.PiExponent.PresentedIdealIso.toIdealModule line 61
5. theorem OAI.PiExponent.PresentedIdealIso.toIdealModule_inclusion line 68
6. instance OAI.PiExponent.PresentedIdealIso.toIdealModule_isIso line 75
7. def OAI.PiExponent.PresentedIdealIso.iso line 108
8. theorem OAI.PiExponent.PresentedIdealIso.iso_hom_inclusion line 116