{R : Ring} (I : Ideal R) : RingHomomorphism R (R / I). Proof. snrapply Build_RingHomomorphism'. 1: rapply grp_quotient_map. repeat split. 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.