proposition: Lemma rng_image_issurj {R S} (f : CRingHomomorphism R S) {issurj : IsSurjection f} : rng_image f ≅ S.
proof: Proof. snrapply Build_CRingIsomorphism. 1: exact (rng_homo_image_incl f). exact _. Defined.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse