{R : Ring} {I : Ideal R} (S : Ring) (f : R $-> S) (H : forall x, I x -> f x = 0) : R / I $-> S. Proof. snrapply Build_RingHomomorphism'. - snrapply (grp_quotient_rec _ _ f). exact H. - split. + srapply QuotientRing_ind2_hprop. nrapply rng_homo_mult. + nrapply rng_homo_one. 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.