instSMul

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

Scalar multiplication by a scalar in 𝕜 acts smoothly on sections.

Русский

Скалярное умножение секунд на скаляр из 𝕜 гладко действует на секциях.

LaTeX

$$$\text{instSMul}$: $\alpha \in 𝕜$, $s \mapsto \alpha \cdot s$ is smooth.$$

Lean4

instance instSMul : SMul 𝕜 Cₛ^n⟮I; F, V⟯ :=
  ⟨fun c s ↦ ⟨c • ⇑s, s.contMDiff.const_smul_section⟩⟩

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

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

Разделы

Аффилиация

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