Finitely generated ideals

Lemmas about finiteness of ideal operations.

theorem Ideal.FG.map {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) : (Ideal.map f I).FG

The image of a finitely generated ideal is finitely generated.

This is the Ideal version of Submodule.FG.map.

theorem Ideal.fg_ker_comp {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [CommRing A] (f : R →+* S) (g : S →+* A) (hf : (RingHom.ker f).FG) (hg : (RingHom.ker g).FG) (hsur : Function.Surjective ⇑f) : (RingHom.ker (g.comp f)).FG

theorem Ideal.exists_radical_pow_le_of_fg {R : Type u_3} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) : ∃ (n : ℕ), I.radical ^ n ≤ I

theorem Ideal.exists_pow_le_of_le_radical_of_fg_radical {R : Type u_3} [CommSemiring R] {I J : Ideal R} (hIJ : I ≤ J.radical) (hJ : J.radical.FG) : ∃ (k : ℕ), I ^ k ≤ J

theorem Ideal.exists_pow_le_of_le_radical_of_fg {R : Type u_3} [CommSemiring R] {I J : Ideal R} (h' : I ≤ J.radical) (h : I.FG) : ∃ (n : ℕ), I ^ n ≤ J