The meta properties of surjective ring homomorphisms. #
theorem
RingHom.surjective_stableUnderComposition :
RingHom.StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
theorem
RingHom.surjective_respectsIso :
RingHom.RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
theorem
RingHom.surjective_stableUnderBaseChange :
RingHom.StableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
theorem
RingHom.surjective_ofLocalizationSpan :
RingHom.OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f