Theorem RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway

Modification history

2024-09-24 15:04
Mathlib/RingTheory/LocalProperties.lean
chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) …
Modified RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAwayView on Github →
2024-09-19 10:59
Mathlib/RingTheory/LocalProperties.lean
chore(AlgebraicGeometry): weaken assumptions on local ring hom properties (#16897) …
Added RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAwayView on Github →