case intro.intro.intro
R : Type ?u.1863870
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1864077
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✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ { x // x ∈ ↑(spanSingleton R₁⁰ (↑(algebraMap R₁ K) d)⁻¹ * ↑J) }
R : Type ?u.1863870
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1864077
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✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
I : FractionalIdeal R₁⁰ K
⊢ IsNoetherian R₁ { x // x ∈ ↑I }
obtain ⟨d, J, _, rfl⟩ := exists_eq_spanSingleton_mul I
case intro.intro.intro.hI
R : Type ?u.1863870
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1864077
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✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ { x // x ∈ ↑↑J }
case intro.intro.intro
R : Type ?u.1863870
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1864077
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✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ { x // x ∈ ↑(spanSingleton R₁⁰ (↑(algebraMap R₁ K) d)⁻¹ * ↑J) }
apply isNoetherian_spanSingleton_inv_to_map_mul
no goals
case intro.intro.intro.hI
R : Type ?u.1863870
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1864077
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✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ { x // x ∈ ↑↑J }
apply isNoetherian_coeIdeal