proposition: Lemma ideal_intersection_subset_product (I J : Ideal R) : ideal_unit R ⊆ (I + J) -> I ∩ J ⊆ I ⋅ J.
proof: Proof. intros p. etransitivity. { apply ideal_eq_subset. symmetry. apply ideal_product_unit_r. } etransitivity. { rapply ideal_product_subset_pres_r. exact p. } rapply ideal_product_intersection_sum_subset'. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups