English
There is a scalar action of a normed field 𝕜 on the space of C^n-maps, i.e., a module structure with r•f defined pointwise and compatible with contMDiff.
Русский
Существует скалярное действие поля 𝕜 на пространство C^n-отображений, образующее модульную структуру, с (r•f)(x)=r·f(x).
LaTeX
$$$\text{instSMul: }\mathfrak{S}: r\cdot f \in C^n(I,N;𝓘(𝕜,V),V)\text{ defined by } (r\cdot f)(x)=r\,f(x).$$$
Lean4
instance semiring {R : Type*} [Semiring R] [TopologicalSpace R] [ChartedSpace H' R] [ContMDiffRing I' n R] :
Semiring C^n⟮I, N; I', R⟯ :=
{ ContMDiffMap.addCommMonoid,
ContMDiffMap.monoid with
left_distrib := fun a b c => by ext; exact left_distrib _ _ _
right_distrib := fun a b c => by ext; exact right_distrib _ _ _
zero_mul := fun a => by ext; exact zero_mul _
mul_zero := fun a => by ext; exact mul_zero _ }
