{R : Ring} (I J : Subgroup R) : Subgroup R := subgroup_leftideal_quotient (R:=rng_op R) I J. Global Instance isrightideal_subgroup_rightideal_quotient {R : Ring} (I J : Subgroup R) `{IsRightIdeal R I} : IsRightIdeal ( I J) := isleftideal_subgroup_leftideal_quotient (R:=rng_op R) I J. Global Instance isleftideal_subgroup_rightideal_quotient {R : Ring} (I J : Subgroup R) `{H : IsLeftIdeal R I, IsRightIdeal R J} : IsLeftIdeal ( I J). Proof. snrapply (isrightideal_subgroup_leftideal_quotient (R:=rng_op R) I J). - exact H. - exact _. Defined.
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.