instDistribMulAction — Mathlib

English

WeakDual inherits a MulAction by M via ContinuousLinearMap.mulAction when M acts on 𝕜 compatibly.

Русский

WeakDual наследует действие умножения от M через ContinuousLinearMap.mulAction при совместимом действии на 𝕜.

LaTeX

$$$\text{WeakDual } 𝕜 E \; \text{is a } M\text{-module via } \text{ContinuousLinearMap.mulAction}$$$

Lean4

/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
multiplication on `𝕜`, then it acts distributively on `WeakDual 𝕜 E`. -/
instance instDistribMulAction (M) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
    DistribMulAction M (WeakDual 𝕜 E) :=
  ContinuousLinearMap.distribMulAction

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