finsupp — Mathlib

English

If ι is finite and M is finitely generated, then the finitely supported functions ι →₀ M are finitely generated as an R-module.

Русский

Если ι конечно и M FG, то модуль ι →₀ M FG.

LaTeX

$$Finite ι ∧ Module.Finite R M ⇒ Module.Finite R (ι →₀ M)$$

Lean4

instance finsupp {ι : Type*} [_root_.Finite ι] [Module.Finite R V] : Module.Finite R (ι →₀ V) :=
  Module.Finite.equiv (Finsupp.linearEquivFunOnFinite R V ι).symm

Похожие утверждения