Commit 2023-06-13 06:31 802488e2

View on Github →

feat: port RingTheory.RingHomProperties (#4404)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHomProperties.lean

added theorem RingHom.RespectsIso.cancel_left_isIso

added theorem RingHom.RespectsIso.cancel_right_isIso

added theorem RingHom.RespectsIso.is_localization_away_iff

added def RingHom.RespectsIso

added theorem RingHom.StableUnderBaseChange.mk

added theorem RingHom.StableUnderBaseChange.pushout_inl

added def RingHom.StableUnderBaseChange

added theorem RingHom.StableUnderComposition.respectsIso

added def RingHom.StableUnderComposition