fact: Definition Coprime {R : CRing} (I J : Ideal R) : Type := ideal_eq (ideal_sum I J) (ideal_unit R).
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups