term_smul — Mathlib

English

For any function f: ℕ → ℂ and any constants c,s ∈ ℂ, the nth term of the scaled sequence c • f equals c times the nth term of f.

Русский

Для любой функции f: ℕ → ℂ и любых констант c,s ∈ ℂ, n-ый член последовательности c • f равен c умножить на n-ый член f.

LaTeX

$$$\forall f:\mathbb{N}\to\mathbb{C},\ c,s\in\mathbb{C},\ term (c\cdot f)\,s = c\cdot (term\,f\,s)$$$

Lean4

theorem term_smul (f : ℕ → ℂ) (c s : ℂ) : term (c • f) s = c • term f s := by ext ⟨- | n⟩ <;> simp [mul_div_assoc]

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