Documentation

Mathlib.RingTheory.RingHom.Surjective

The meta properties of surjective ring homomorphisms. #

source
theorem RingHom.surjective_stableUnderComposition :
RingHom.StableUnderComposition fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f
source
theorem RingHom.surjective_respectsIso :
RingHom.RespectsIso fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f
source
theorem RingHom.surjective_stableUnderBaseChange :
RingHom.StableUnderBaseChange fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f
source
theorem RingHom.surjective_ofLocalizationSpan :
RingHom.OfLocalizationSpan fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) => Function.Surjective ⇑f