def TwoSidedIdeal.moduleAnnihilator (R : Type u_2) [Ring R] (M : Type u_3) [AddCommGroup M] [Module R M] : TwoSidedIdeal R

def TwoSidedIdeal.IsPrimitive {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Prop