proposition: Lemma ideal_quotient_sum (I J K : Ideal R) : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
proof: Proof. apply ideal_subset_antisymm. { intros r p; split. + intros x j. hnf in p; apply p. by apply ideal_sum_subset_l. + intros x k. hnf in p; apply p. by apply ideal_sum_subset_r. } intros r [p q] x jk. hnf in p, q. strip_truncations. induction jk as [s x | | ]. - destruct x. 1: by apply p. by apply q. - rewrite rng_mult_zero_r. apply ideal_in_zero. - rewrite rng_dist_l. rewrite rng_mult_negate_r. by apply ideal_in_plus_negate. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups