OAI/NumberTheory/PiExponent/LocalAlgebra/IdealPullbackOpenSquare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.IdealSectionRestriction.bijective_iff_of_square line 10
2. theorem OAI.PiExponent.IdealSectionRestriction.appLE_congr line 18
3. theorem OAI.PiExponent.IdealSectionRestriction.squareIdeal line 24
4. theorem OAI.PiExponent.IdealSectionRestriction.pullback_open_square line 30
5. theorem OAI.PiExponent.IdealSectionRestriction.pullback_open_square_bijective_iff line 59
6. theorem OAI.PiExponent.IdealSectionRestriction.comap_app_bijective_iff_open_square line 79