rng_first_iso' `{Funext} {A B : Ring} (f : A $-> B) (issurj_f : IsSurjection f) (I : Ideal A) (p : (I ↔ ideal_kernel f)%ideal) : A / I ≅ B. Proof. etransitivity. 1: apply (rng_quotient_invar p). etransitivity. 2: rapply (rng_image_issurj f). apply rng_first_iso. Defined.
Require Import WildCat.Core WildCat.Equiv. Require Import Algebra.Congruence. Require Import Algebra.AbGroups. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Rings.Ring. Require Import Algebra.Rings.Ideal. Import Ideal.Notation.