fact: Definition ideal_annihilator `{Funext} {R : CRing} (I : Ideal R) : Ideal R := ideal_quotient (ideal_zero R) I.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups