The meta properties of surjective ring homomorphisms. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
ring_hom.surjective_stable_under_composition
:
ring_hom.stable_under_composition (λ {X Y : Type u_1} [_inst_1 : comm_ring X] [_inst_2 : comm_ring Y] (f : X →+* Y), function.surjective ⇑f)
theorem
ring_hom.surjective_respects_iso
:
ring_hom.respects_iso (λ {X Y : Type u_1} [_inst_1 : comm_ring X] [_inst_2 : comm_ring Y] (f : X →+* Y), function.surjective ⇑f)
theorem
ring_hom.surjective_stable_under_base_change
:
ring_hom.stable_under_base_change (λ {X Y : Type u_1} [_inst_1 : comm_ring X] [_inst_2 : comm_ring Y] (f : X →+* Y), function.surjective ⇑f)
theorem
ring_hom.surjective_of_localization_span
:
ring_hom.of_localization_span (λ {X Y : Type u_1} [_inst_1 : comm_ring X] [_inst_2 : comm_ring Y] (f : X →+* Y), function.surjective ⇑f)