fact: Record Ideal (R : CRing) := { ideal_subgroup : Subgroup R; ideal_isideal : IsIdeal ideal_subgroup; }.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups