mathlib3 documentation

ring_theory.ring_hom.surjective

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_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)