{R : Ring} (I J : Subgroup R) : Subgroup R. Proof. snrapply Build_Subgroup'. - exact (fun r => merely (forall x, J x -> I (r * x))). - exact _. - apply tr. intros r p. rewrite rng_mult_zero_l. apply ideal_in_zero. - intros x y p q. strip_truncations; apply tr. hnf; intros s j. rewrite rng_dist_r. rewrite rng_mult_negate_l. apply ideal_in_plus_negate. + by apply p. + by apply q. 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.