instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2

English

The commutativity of scalar actions extends to the Lp-subtype space, showing compatibility of the DomMulAct action with the scalar field 𝕜.

Русский

Коммутативность действий скаляра распространяется на Lp-подпространство; совместимость DomMulAct с 𝕜.

LaTeX

$$SMulCommClass 𝕜 (DomMulAct M) (Subtype fun x => SetLike.instMembership.mem (MeasureTheory.Lp E p μ) x)$$

Lean4

instance {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : SMulCommClass 𝕜 Mᵈᵐᵃ (Lp E p μ) :=
  .symm _ _
    _
      -- We don't have a typeclass for additive versions of the next few lemmas
      -- Should we add `AddDistribAddAction` with `to_additive` both from `MulDistribMulAction`
      -- and `DistribMulAction`?

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