instMulAction

Mathlib.Analysis.Normed.Lp.WithLp

URI: https://scilib.ai/kg/mathlib#WithLp.instMulAction

English

If K is a Monoid and V has a K-action, then WithLp p V inherits a natural K-action from V.

Русский

Пусть K — моноид и V имеет действие K. Тогда WithLp p V наследует естественное действие K от V.

LaTeX

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

Lean4

@[to_additive]
instance instMulAction [Monoid K] [MulAction K V] : MulAction K V :=
  ‹MulAction K V›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru