Theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffine

Modification history

2024-03-02 20:50
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
refactor: deprecate duplicated RespectsIso theorem (#11115) …
Deleted RingHom.RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffineView on Github →
2023-10-19 12:40
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
feat(Mathlib/AlgebraicGeometry): Move material on restriction to new file (#7749) …
Added RingHom.RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffineView on Github →