proposition: Lemma ideal_dist_r (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
proof: Proof. apply ideal_subset_antisymm. { intros r p. strip_truncations. induction p as [ r i | | r s p1 IHp1 p2 IHp2]. - destruct i as [r s p q]. strip_truncations. induction p as [ t k | | t k p1 IHp1 p2 IHp2 ]. + apply tr, sgt_in. destruct k as [j | k]. * left; by apply tr, sgt_in, ipn_in. * right; by apply tr, sgt_in, ipn_in. + apply tr, sgt_in; left. rewrite rng_mult_zero_l. apply ideal_in_zero. + rewrite rng_dist_r. rewrite rng_mult_negate_l. by apply ideal_in_plus_negate. - apply ideal_in_zero. - by apply ideal_in_plus_negate. } apply ideal_sum_smallest. 1,2: apply ideal_product_subset_pres_l. 1: apply ideal_sum_subset_l. apply ideal_sum_subset_r. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups