{R : CRing} (I : Ideal R) : R $-> cring_quotient R I := rng_quotient_map I.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.