(I J : Ideal R) : I ⋅ J ↔ J ⋅ I. Proof. apply ideal_subset_antisymm; apply ideal_product_subset_product_commutative. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.