R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ WellFounded fun x x_1 => x < x_1
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ IsArtinian R M
rw [isArtinian_iff_wellFounded]
no goals
R : Type u_2
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → ↑f n = ↑f m) ↔ WellFounded fun x x_1 => x < x_1
exact WellFounded.monotone_chain_condition.symm