instSMulCommClass — Mathlib

English

An instance stating Lp has a central scalar action from 𝕜.

Русский

Экземпляр утверждает, что Lp имеет центральное скалярное действие от 𝕜.

LaTeX

$$$[IsCentralScalar 𝕜 E] \Rightarrow IsCentralScalar 𝕜 (Lp E p μ)$$$

Lean4

instance instSMulCommClass [SMulCommClass 𝕜 𝕜' E] : SMulCommClass 𝕜 𝕜' (Lp E p μ) where
  smul_comm k k' f := Subtype.ext <| smul_comm k k' (f : α →ₘ[μ] E)

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