Commit 2024-03-02 20:50 cddd40b1
View on Github →refactor: deprecate duplicated RespectsIso theorem (#11115)
Deprecates RespectsIso.ofRestrict_morphismRestrict_iff_of_isAffine in favor of the older RespectsIso.basicOpen_iff_localization, and removes a local notation that is only used in the removed proof.