{R S} (f : RingHomomorphism R S) {issurj : IsSurjection f} : (rng_image f : Ring) ≅ S. Proof. snrapply Build_RingIsomorphism. 1: exact (rng_homo_image_incl f). exact _. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.