fact: Definition ideal_intersection {R : CRing} : Ideal R -> Ideal R -> Ideal R := fun I J => Build_Ideal R _ (isideal_subgroup_intersection R I J).
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups