instModuleFinite — Mathlib

English

If V is a Module over K and Module.Finite K V holds, then WithLp p V is Module.Finite over K as well.

Русский

Если V является модулем над K и выполняется Module.Finite K V, то WithLp p V также является Module.Finite над K.

LaTeX

$$$[Module.Finite K V] \Rightarrow Module.Finite K (WithLp p V)$$$

Lean4

instance instModuleFinite [Semiring K] [AddCommGroup V] [Module K V] [Module.Finite K V] :
    Module.Finite K (WithLp p V) :=
  ‹Module.Finite K V›

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