const_mul — Mathlib

English

If f is a function AddCircle T → ℂ and c ∈ ℂ, then the Fourier coefficient of the function x ↦ c·f(x) equals c times the Fourier coefficient of f.

Русский

Если f — функция AddCircle T → ℂ и c ∈ ℂ, то коэффициент Фурье функции x ↦ c·f(x) равен c умножить на коэффициент Фурье f.

LaTeX

$$$$ \\widehat{(c\\cdot f)}_n = c\\cdot \\widehat{f}_n $$$$

Lean4

theorem const_mul (f : AddCircle T → ℂ) (c : ℂ) (n : ℤ) : fourierCoeff (fun x => c * f x) n = c * fourierCoeff f n :=
  fourierCoeff.const_smul f c n

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