English
IsFiniteLength(R,M) holds if and only if M is Noetherian and Artinian as an R-module.
Русский
IsFiniteLength(R,M) эквивалентно тому, что M является Noetherian и Artinian как R-модуль.
LaTeX
$$$\\operatorname{IsFiniteLength} R M \\iff (\\operatorname{IsNoetherian} R M \\land \\operatorname{IsArtinian} R M)$$$
Lean4
theorem isFiniteLength_iff_isNoetherian_isArtinian : IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M :=
open scoped IsSimpleOrder in
⟨fun h ↦
h.rec (fun {M} _ _ _ ↦ ⟨inferInstance, inferInstance⟩) fun M _ _ {N} _ _ ⟨_, _⟩ ↦
⟨(isNoetherian_iff_submodule_quotient N).mpr ⟨‹_›, isNoetherian_iff'.mpr inferInstance⟩,
(isArtinian_iff_submodule_quotient N).mpr ⟨‹_›, inferInstance⟩⟩,
fun ⟨_, _⟩ ↦ isFiniteLength_of_exists_compositionSeries (exists_compositionSeries_of_isNoetherian_isArtinian R M)⟩
