R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
f : R →+* S
hf : Surjective ↑f
H : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
f : R →+* S
hf : Surjective ↑f
H : IsNoetherianRing R
⊢ IsNoetherianRing S
rw [isNoetherianRing_iff, isNoetherian_iff_wellFounded] at H⊢
no goals
R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
f : R →+* S
hf : Surjective ↑f
H : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
exact OrderEmbedding.wellFounded (Ideal.orderEmbeddingOfSurjective f hf).dual H