English
If M ≃ₗ[R] N is a linear equivalence and M has finite length, then N has finite length.
Русский
Если M и N линейно эквивалентны через e: M ≃ₗ[R] N, и M имеет конечную длину, то и N имеет конечную длину.
LaTeX
$$$e : M \\simeq_{\\!R} N \\quad\\Rightarrow\\quad \\operatorname{IsFiniteLength} R M \\rightarrow \\operatorname{IsFiniteLength} R N$$$
Lean4
theorem isFiniteLength (e : M ≃ₗ[R] N) (h : IsFiniteLength R M) : IsFiniteLength R N := by
induction h generalizing N with
| of_subsingleton => have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
| @of_simple_quotient M _ _ S _ _
ih =>
have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
exact .of_simple_quotient (ih <| e.submoduleMap S)
