(I J : Ideal R) : Coprime I J -> I ∩ J ↔ I ⋅ J. Proof. intros p. apply ideal_subset_antisymm. - apply ideal_intersection_subset_product. unfold Coprime in p. apply symmetry in p. rapply p. - apply ideal_product_subset_intersection. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.