R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ (J : FractionalIdeal R₁⁰ K), J ≤ ↑I → FG ↑J
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ IsNoetherian R₁ { x // x ∈ ↑↑I }
rw [isNoetherian_iff]
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal R₁⁰ K
hJ : J ≤ ↑I
⊢ FG ↑J
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ (J : FractionalIdeal R₁⁰ K), J ≤ ↑I → FG ↑J
intro J hJ
case intro
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I J : Ideal R₁
hJ : ↑J ≤ ↑I
⊢ FG ↑↑J
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal R₁⁰ K
hJ : J ≤ ↑I
⊢ FG ↑J
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)
no goals
case intro
R : Type ?u.1753199
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1753406
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsNoetherianRing R₁
I J : Ideal R₁
hJ : ↑J ≤ ↑I
⊢ FG ↑↑J
exact (IsNoetherian.noetherian J).map _