instSMul — Mathlib

English

If R acts on M and there is a continuous scalar multiplication, then R acts on C(α, M) by (r • f)(x) = r • f(x).

Русский

Если R действует на M и есть непрерывное наслоение скаляра, то R действует на C(α, M) по формулам (r•f)(x)=r•f(x).

LaTeX

$$$ (r,f) \mapsto (x \mapsto r\cdot f(x)) \in C(α,M) $ defines an action of R on C(α,M). $$

Lean4

@[to_additive]
instance instSMul [SMul R M] [ContinuousConstSMul R M] : SMul R C(α, M) :=
  ⟨fun r f => ⟨r • ⇑f, f.continuous.const_smul r⟩⟩

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