no goals
R : Type u_2
M : Type u_1
P : Type ?u.118511
N : Type w
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∀ (a : Set (Submodule R M)), Set.Nonempty a → ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), I ∈ a → ¬M' < I) ↔
    IsNoetherian R M
rw [isNoetherian_iff_wellFounded, WellFounded.wellFounded_iff_has_min]