{R : Ring} (I J : Subgroup R) : Subgroup R := subgroup_generated (G := R) (ideal_product_naive_type I J). Global Instance isleftideal_ideal_product_type {R : Ring} (I J : Subgroup R) `{IsLeftIdeal R I, IsLeftIdeal R J} : IsLeftIdeal ( I J). Proof. intro r. nrapply (functor_subgroup_generated _ _ (grp_homo_rng_left_mult r)). intros s [s1 s2 p1 p2]; cbn. rewrite simple_associativity. nrefine (ipn_in I J (r * s1) s2 _ p2). by apply isleftideal. 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.