{R : Ring} (I : RightIdeal R) : Ideal R := Build_Ideal R (subgroup_ideal_right_annihilator (R:=R) I) (isideal_ideal_right_annihilator (R:=R) I).
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.