coe_nsmul — Mathlib

English

For n ∈ ℕ, the coercion respects natural-scalar multiplication: (n • f) as a function equals n • (f as function).

Русский

Приведение к функции сохраняет умножение на естественные числа: (n • f) как функция равно n • (f как функция).

LaTeX

$$$\forall n \in \mathbb{N}:\ (n \cdot f) = n \cdot (f)$ as functions$$

Lean4

@[norm_cast, simp]
theorem coe_nsmul (n : ℕ) (f : M →ₗ⁅R,L⁆ N) : ⇑(n • f) = n • (⇑f) :=
  rfl

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