OAI/NumberTheory/PiExponent/LocalAlgebra/SectionImageIdeal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.SectionImageIdeal.imageIdeal line 12
2. lemma OAI.PiExponent.SectionImageIdeal.map_imageIdeal_le line 15
3. theorem OAI.PiExponent.SectionImageIdeal.affine_map_imageIdeal line 22
4. theorem OAI.PiExponent.SectionImageIdeal.imageIdeal_restrict line 46
5. theorem OAI.PiExponent.SectionImageIdeal.map_imageIdeal_affine_image line 68
6. theorem OAI.PiExponent.SectionImageIdeal.map_imageIdeal_basicOpen line 86
7. def OAI.PiExponent.SectionImageIdeal.imageIdealSheaf line 100
8. theorem OAI.PiExponent.SectionImageIdeal.imageIdealSheaf_ideal line 104
9. theorem OAI.PiExponent.SectionImageIdeal.imageIdeal_top_of_frame line 108
10. lemma OAI.PiExponent.SectionImageIdeal.imageIdeal_map_eq line 126
11. theorem OAI.PiExponent.SectionImageIdeal.imageIdealSheaf_on_frame line 133