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