proposition: Lemma ideal_product_comm (I J : Ideal R) : I ⋅ J ↔ J ⋅ I.
proof: Proof. assert (p : forall K L : Ideal R, K ⋅ L ⊆ L ⋅ K). { clear I J; intros I J. intros r p. strip_truncations. induction p as [r p | |]. 2: apply ideal_in_zero. 2: by apply ideal_in_plus_negate. destruct p as [s t p q]. rewrite rng_mult_comm. by apply tr, sgt_in, ipn_in. } apply ideal_subset_antisymm; apply p. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups