instStarModule — Mathlib

English

There is a StarModule structure on C_c(α,β) letting the scalar action interact with star and addition componentwise.

Русский

Существует структура StarModule на C_c(α,β), где скалярное действие взаимодействует со звездой и сложением по компонентам.

LaTeX

$$$\text{instStarModule}:\ StarModule 𝕜 \, C_c(α,β)$$$

Lean4

instance : StarModule 𝕜 C_c(α, β) where star_smul k f := ext fun x => star_smul k (f x)

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