coe_nsmul

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

← MathLib Explorer

English

Integer scalar multiplication is smooth.

Русский

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

LaTeX

$$$\text{instZSMul}$: $ z \in \mathbb{Z} \mapsto z\cdot s$ is ContMDiff.$$

Lean4

@[simp]
theorem coe_nsmul (s : Cₛ^n⟮I; F, V⟯) (k : ℕ) : ⇑(k • s : Cₛ^n⟮I; F, V⟯) = k • ⇑s := by
  induction k with
  | zero => simp_rw [zero_smul]; rfl
  | succ k ih => simp_rw [succ_nsmul, ← ih]; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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