English
The SMul' instance provides a natural action of C^n-valued scalar maps on C^n-valued maps with values in V by pointwise multiplication.
Русский
Инстанс SMul' задаёт естественное действие отображений C^n(I,N; 𝓘(𝕜,V),V) на C^n(I,N; 𝓘(𝕜,V),V) по точкам.
LaTeX
$$$\\text{SMul'}\\;: \\mathrm{C^n(I,N; 𝓘(𝕜,V),V)} \\times \\mathrm{C^n(I,N; 𝓘(𝕜,V),V)} \\to \\mathrm{C^n(I,N; 𝓘(𝕜,V),V)},\\; (f,g)\\mapsto (x\\mapsto f(x)\\,g(x)).$$$
Lean4
/-- The space of `C^n` functions with values in a space `V` is a module over the space of `C^n`
functions with values in `𝕜`. -/
instance module' {V : Type*} [NormedAddCommGroup V] [NormedSpace 𝕜 V] : Module C^n⟮I, N; 𝓘(𝕜), 𝕜⟯ C^n⟮I, N; 𝓘(𝕜, V), V⟯
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 𝕜 (f x)
zero_smul f := by ext x; exact zero_smul _ _
smul_zero r := by ext x; exact smul_zero _
