(I J K : Ideal R) : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K). Proof. apply ideal_subset_antisymm. { intros r [p q]; strip_truncations; split; split; apply tr; intros x jk. - by rapply p; rapply ideal_sum_subset_l. - by rapply q; rapply ideal_sum_subset_l. - by rapply p; rapply ideal_sum_subset_r. - by rapply q; rapply ideal_sum_subset_r. } intros r [[p q] [u v]]; strip_truncations; split; apply tr; intros x jk; strip_truncations. - induction jk as [? [] | | ? ? ? ? ? ? ]. + by apply p. + by apply u. + apply u, ideal_in_zero. + rewrite rng_dist_l. rewrite rng_mult_negate_r. by apply ideal_in_plus_negate. - induction jk as [? [] | | ? ? ? ? ? ? ]. + by apply q. + by apply v. + apply v, ideal_in_zero. + change (I ((g - h) * r)). rewrite rng_dist_r. rewrite rng_mult_negate_l. by apply ideal_in_plus_negate. Defined.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.