OAI/NumberTheory/PiExponent/LocalAlgebra/InvertibleIdealAway.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.InvertibleIdealAway.isIso_of_comp_iso_hom line 14
2. theorem OAI.PiExponent.InvertibleIdealAway.restrictedInclusion_isIso_of_unit line 18
3. theorem OAI.PiExponent.InvertibleIdealAway.inclusion_isIso_of_comap_top line 46
4. theorem OAI.PiExponent.InvertibleIdealAway.pullback_map_isIso_of_factors line 62
5. theorem OAI.PiExponent.InvertibleIdealAway.pullback_inclusion_isIso_of_avoids line 77
6. def OAI.PiExponent.InvertibleIdealAway.pullbackInclusion line 100
7. def OAI.PiExponent.InvertibleIdealAway.pullbackIsoOfAvoids line 104
8. def OAI.PiExponent.InvertibleIdealAway.pullbackIsoOfComapTop line 113