OAI/NumberTheory/PiExponent/LocalAlgebra/AffineIdealSections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.GeometrySupport.AffineIdealSections.value line 11
2. theorem OAI.PiExponent.GeometrySupport.AffineIdealSections.value_mem line 15
3. def OAI.PiExponent.GeometrySupport.AffineIdealSections.toIdeal line 26
4. theorem OAI.PiExponent.GeometrySupport.AffineIdealSections.toIdeal_injective line 39
5. theorem OAI.PiExponent.GeometrySupport.AffineIdealSections.toIdeal_surjective line 52
6. def OAI.PiExponent.GeometrySupport.AffineIdealSections.equiv line 69
7. theorem OAI.PiExponent.GeometrySupport.AffineIdealSections.equiv_inclusion line 72
8. theorem OAI.PiExponent.GeometrySupport.AffineIdealSections.equiv_symm_inclusion line 76