instZSMul

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

Natural-number scalar multiple of a smooth section is smooth.

Русский

Умножение секции на натуральное число гладко.

LaTeX

$$$\text{instNSMul}$: $k \cdot s$ smooth for $k \in \mathbb{N}$.$$

Lean4

instance instZSMul : SMul ℤ Cₛ^n⟮I; F, V⟯ :=
  ⟨zsmulRec⟩

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

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

Разделы

Аффилиация

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