instStarModule — Mathlib

English

If R is a StarRing with ContinuousStar and M acts suitably, then C(X, R)₀ is a StarModule over M, with star-scalar action defined pointwise.

Русский

Если R имеет непрерывное сопряжение и M действует над R, то C(X, R)₀ образует StarModule над M, с определением звёздного действия по точкам.

LaTeX

$$$\text{StarModule } M\ (\text{ContinuousMapZero } X\ R)\ R$$$

Lean4

instance instStarModule [StarRing R] {M : Type*} [SMulZeroClass M R] [ContinuousConstSMul M R] [Star M] [StarModule M R]
    [ContinuousStar R] : StarModule M C(X, R)₀ where star_smul r f := ext fun x ↦ star_smul r (f x)

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