{R : Ring} : Ideal R -> Ideal R -> Ideal R := fun I J => Build_Ideal R (ideal_product_type I J) _. Global Instance isleftideal_grp_kernel {R S : Ring} (f : RingHomomorphism R S) : IsLeftIdeal (grp_kernel f). Proof. intros r x p. lhs nrapply rng_homo_mult. rhs_V nrapply (rng_mult_zero_r (f r)). by apply ap. 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.