English
The space of C^n-valued smooth maps with values in a normed algebra A carries a natural algebra structure over the base field 𝕜, with pointwise addition, multiplication, and scalar multiplication; the algebra map is given by evaluation into A.
Русский
Множество C^n-дифференцируемых отображений, принимающих значения в нормированном алгебре A, естественно образует 𝕜-алгебру; операции сложения, умножения и скалярного умножения выполняются по точкам; алгебраическое отображение задаётся отображением в A.
LaTeX
$$$\\text{Algebra}_{\\mathbb{k}}(\\mathrm{C^n(I,N; 𝓘(\\mathbb{k},A),A)})$$$
Lean4
instance algebra : Algebra 𝕜 C^n⟮I, N; 𝓘(𝕜, A), A⟯
where
smul := fun r f => ⟨r • f, contMDiff_const.smul f.contMDiff⟩
algebraMap := ContMDiffMap.C
commutes' := fun c f => by ext x; exact Algebra.commutes' _ _
smul_def' := fun c f => by ext x; exact Algebra.smul_def' _ _
