R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : SMul R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : SMul R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : IsNoetherian R M
⊢ IsNoetherian S M
rw [isNoetherian_iff_wellFounded] at h⊢
no goals
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : SMul R S
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
refine' (Submodule.restrictScalarsEmbedding R S M).dual.wellFounded h