English
The length not equal to top is equivalent to having finite length (IsFiniteLength).
Русский
Длина не равна топу эквивалентна существованию конечной длины.
LaTeX
$$$\operatorname{length}(R,M) \neq \top \iff \operatorname{IsFiniteLength} R M.$$$
Lean4
theorem length_ne_top_iff : Module.length R M ≠ ⊤ ↔ IsFiniteLength R M :=
by
refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
· rw [length_ne_top_iff_finiteDimensionalOrder] at h
rw [isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff, isArtinian_iff]
let R : SetRel (Submodule R M) (Submodule R M) := {(N₁, N₂) : Submodule R M × Submodule R M | N₁ < N₂}
change R.inv.IsWellFounded ∧ R.IsWellFounded
exact ⟨.of_finiteDimensional R.inv, .of_finiteDimensional R⟩
· obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H
rw [← length_compositionSeries s hs₁ hs₂]
simp
