English
If M is finite over R and f: M → N is linear, then the range (image) of f is finite as an R–module.
Русский
Если M является конечным модулем над R и f: M → N линейно отображает, то образ f в N является конечным как R- модуль.
LaTeX
$$$\\forall R\\,M\\,N\\; [\\text{Module } R M]\, [\\text{Module } R N]\, [\\text{Module.Finite } R M]\, (f: M \\to N)\\;\\Rightarrow\\; \\text{Module.Finite } R (\\mathrm{range}(f))$$
Lean4
/-- The range of a linear map from a finite module is finite. -/
instance range {F : Type*} [FunLike F M N] [SemilinearMapClass F (RingHom.id R) M N] [Module.Finite R M] (f : F) :
Module.Finite R (LinearMap.range f) :=
of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩
