{R : Ring} : Ideal R -> Ideal R -> Ideal R := fun I J => Build_Ideal R (subgroup_intersection I J) _. Global Instance isleftideal_subgroup_product (R : Ring) (I J : Subgroup R) `{IsLeftIdeal R I, IsLeftIdeal R J} : IsLeftIdeal (subgroup_product I J). Proof. intros r. nrapply subgroup_product_ind. - intros x p. apply tr, sgt_in. left; by apply isleftideal. - intros x p. apply tr, sgt_in. right; by apply isleftideal. - apply tr, sgt_in. left; apply isleftideal. apply ideal_in_zero. - intros x y p q IHp IHq; cbn beta. rewrite rng_dist_l. rewrite rng_mult_negate_r. by apply subgroup_in_op_inv. - 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.