instModule — Mathlib

English

If K is a Semiring and V is an AddCommGroup with a K-Module structure, then WithLp p V becomes a Module K (WithLp p V).

Русский

Если K — полугруппа и V — AddCommGroup с модульной структурой над K, то WithLp p V становится модулем над K.

LaTeX

$$$[Semiring K] [AddCommGroup V] [Module K V] \Rightarrow Module K (WithLp p V)$$$

Lean4

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

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