proposition: Lemma ideal_product_subset_intersection (I J : Ideal R) : I ⋅ J ⊆ I ∩ J.
proof: Proof. apply ideal_intersection_subset. + apply ideal_product_subset_l. + apply ideal_product_subset_r. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups