proposition: Lemma ideal_product_intersection_sum_subset' (I J : Ideal R) : (I ∩ J) ⋅ (I + J) ⊆ I ⋅ J.
proof: Proof. etransitivity. 2: rapply ideal_sum_self. etransitivity. 2: rapply ideal_sum_subset_pres_r. 2: rapply ideal_product_comm. apply ideal_product_intersection_sum_subset. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups