instDistribMulAction — Mathlib

English

If K is a Monoid, V is an AddCommGroup and DistribMulAction K V holds, then WithLp p V carries a DistribMulAction K as well.

Русский

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

LaTeX

$$$[Monoid K] [AddCommGroup V] [DistribMulAction K V] \Rightarrow DistribMulAction K (WithLp p V)$$$

Lean4

instance instDistribMulAction [Monoid K] [AddCommGroup V] [DistribMulAction K V] : DistribMulAction K (WithLp p V) :=
  ‹DistribMulAction K V›

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