Theorem RingHom.StableUnderCompositionWithLocalizationAway.respectsIso

Modification history

2024-10-15 08:21
Mathlib/RingTheory/LocalProperties/Basic.lean
feat(RingTheory/Locally): stability properties of `Locally P` (#17335) …
Added RingHom.StableUnderCompositionWithLocalizationAway.respectsIsoView on Github →