instModule' — Mathlib

English

WeakDual supports an R-module structure when R, 𝕜 and action compatibilities hold.

Русский

WeakDual обладает структурой модуля над R при совместимости действий.

LaTeX

$$$\text{WeakDual } 𝕜 E \text{ is an } R\text{-module under the given assumptions}$$$

Lean4

/-- If `𝕜` is a topological module over a semiring `R` and scalar multiplication commutes with the
multiplication on `𝕜`, then `WeakDual 𝕜 E` is a module over `R`. -/
instance instModule' (R) [Semiring R] [Module R 𝕜] [SMulCommClass 𝕜 R 𝕜] [ContinuousConstSMul R 𝕜] :
    Module R (WeakDual 𝕜 E) :=
  ContinuousLinearMap.module

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