{R S : Ring} (f : R $-> S) (I : Ideal R) : Ideal S := ideal_generated (fun s => exists r, I r /\ f r = s).
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.