English
There is a module structure of C(α,R) acting on C(α,M) making them a module over the ring C(α,R) given by pointwise multiplication.
Русский
Существует структура модуля на паре C(α,R) и C(α,M), которая делает их модулем над кольцом C(α,R) через точечное умножение.
LaTeX
$$$\\text{Module on } C(α,R) \\text{ over } C(α,M) : \\text{module with } (f,g) \\mapsto (x \\mapsto f(x)g(x)).$$$
Lean4
instance module' [IsTopologicalSemiring R] [ContinuousAdd M] : Module C(α, R) C(α, M)
where
smul := (· • ·)
smul_add c f g := by ext x; exact smul_add (c x) (f x) (g x)
add_smul c₁ c₂ f := by ext x; exact add_smul (c₁ x) (c₂ x) (f x)
mul_smul c₁ c₂ f := by ext x; exact mul_smul (c₁ x) (c₂ x) (f x)
one_smul f := by ext x; exact one_smul R (f x)
zero_smul f := by ext x; exact zero_smul _ _
smul_zero r := by ext x; exact smul_zero _
