instSMulCommClass — Mathlib

English

If there are commuting scalar actions on V by K and K', then the same SMulCommClass holds for WithLp p V.

Русский

Если скалярные действия на V по K и K' коммьютируются, то для WithLp p V выполняется аналогичное свойство SMulCommClass.

LaTeX

$$$SMulCommClass K K' (WithLp p V)$$$

Lean4

@[to_additive]
instance instSMulCommClass [SMul K V] [SMul K' V] [SMulCommClass K K' V] : SMulCommClass K K' (WithLp p V) :=
  ‹SMulCommClass K K' V›

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