case mp
R : Type u_1
M : Type u_2
P : Type ?u.20594
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R { x // x ∈ ⊤ }
⊢ IsNoetherian R M

case mpr
R : Type u_1
M : Type u_2
P : Type ?u.20594
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R M
⊢ IsNoetherian R { x // x ∈ ⊤ }
R : Type u_1
M : Type u_2
P : Type ?u.20594
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
⊢ IsNoetherian R { x // x ∈ ⊤ } ↔ IsNoetherian R M
constructor <;> intro h
no goals
case mp
R : Type u_1
M : Type u_2
P : Type ?u.20594
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R { x // x ∈ ⊤ }
⊢ IsNoetherian R M
exact isNoetherian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl)
no goals
case mpr
R : Type u_1
M : Type u_2
P : Type ?u.20594
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
h : IsNoetherian R M
⊢ IsNoetherian R { x // x ∈ ⊤ }
exact isNoetherian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl).symm