{R : Ring} (I : Subgroup R) : _ <~> IsIdeal I := ltac:(issig). Hint Immediate Build_IsIdeal : typeclass_instances. Global Instance isideal_op {R : Ring} (I : Subgroup R) : IsIdeal I -> IsIdeal (R := rng_op R) I. Proof. intros [? ?]; 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.