coe_smul — Mathlib

English

Let s be a smooth (C^n) section of a vector bundle and r a scalar. The underlying function of the scalar-multiplied section is the scalar multiple of the underlying function: ev(r · s) = r · ev(s).

Русский

Пусть s — гладкая секция векторного расслоения и r — скаляр. Функция, соответствующая секции r · s, равна в точности r, умножающему значения секции: ev(r · s) = r · ev(s).

LaTeX

$$$$\mathrm{ev}(r \cdot s) = r\,\mathrm{ev}(s).$$$$

Lean4

@[simp]
theorem coe_smul (r : 𝕜) (s : Cₛ^n⟮I; F, V⟯) : ⇑(r • s : Cₛ^n⟮I; F, V⟯) = r • ⇑s :=
  rfl

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