Commit 2024-10-15 08:21 196b03b8

View on Github →

feat(RingTheory/Locally): stability properties of Locally P (#17335) If a property of ring homomorphisms P is stable under base-change, composition, localizations, etc. then so is Locally P.

Estimated changes

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

added theorem RingHom.StableUnderCompositionWithLocalizationAway.respectsIso

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/RingHom/Locally.lean

added theorem RingHom.locally_holdsForLocalizationAway

added theorem RingHom.locally_localizationPreserves

added theorem RingHom.locally_propertyIsLocal

added theorem RingHom.locally_respectsIso

added theorem RingHom.locally_stableUnderBaseChange

added theorem RingHom.locally_stableUnderComposition

added theorem RingHom.locally_stableUnderCompositionWithLocalizationAway