instStarModule — Mathlib

English

If R is a ring with a star structure and a compatible module action on β, then the function space C(α, β) becomes a StarModule with star acting diagonally: star(k·f) = k·f^*.

Русский

Если R — кольцо со звездой и есть согласованное действие модуля на β, то C(α, β) становится StarModule: звезда скалярного умножения действует по диагонали.

LaTeX

$$$\mathrm{StarModule}\bigl(R, C(\alpha, \beta)\bigr)$ with $\star\,(k\cdot f)=k\cdot f^*$$$

Lean4

instance [Star R] [Star β] [SMul R β] [StarModule R β] [ContinuousStar β] [ContinuousConstSMul R β] :
    StarModule R C(α, β) where star_smul _ _ := ext fun _ => star_smul _ _

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