instSMul

Mathlib.Topology.ContinuousMap.ContinuousMapZero

URI: https://scilib.ai/kg/mathlib#ContinuousMapZero.instSMul

English

There is an action of a ring M on ContinuousMapZero X R given by (m • f)(x) = m • f(x).

Русский

Существует действие кольца M на ContinuousMapZero X R: (m • f)(x) = m • f(x).

LaTeX

$$ (m • f)(x) = m • f(x) $$

Lean4

instance instSMul {M : Type*} [Zero R] [SMulZeroClass M R] [ContinuousConstSMul M R] : SMul M C(X, R)₀ where
  smul m f := ⟨m • f, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru