proposition: Lemma rng_quotient_invar {R : CRing} {I J : Ideal R} (p : (I ↔ J)%ideal) : R / I ≅ R / J.
proof: Proof. snrapply Build_CRingIsomorphism'. { srapply equiv_quotient_functor'. 1: exact equiv_idmap. intros x y; cbn. apply p. } repeat split. 1,2: intros x; simpl. 1,2: srapply QuotientRing_ind_hprop. 1,2: intros y; revert x. 1,2: srapply QuotientRing_ind_hprop. 1,2: intros x; rapply qglue. 1: change (J ( - (x + y) + (x + y))). 2: change (J (- ( x * y) + (x * y))). 1,2: rewrite rng_plus_negate_l. 1,2: apply ideal_in_zero. Defined.
imports: WildCat Algebra.Congruence Algebra.AbGroups Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.Rings.Ideal