fourier_neg' — Mathlib

English

For every n ∈ ℤ and x ∈ AddCircle(T), the negated monomial equals conj of the original: f_{-n}(x) = conj(f_n(x)).

Русский

Для каждого n ∈ ℤ и x ∈ AddCircle(T) мономиала с индексом −n равна conj(f_n(x)).

LaTeX

$$$f_{-n}(x) = \\overline{f_n(x)}$ for all $n \\in \\mathbb{Z}$, $x \\in AddCircle(T).$$$

Lean4

@[simp]
theorem fourier_neg' {n : ℤ} {x : AddCircle T} : @toCircle T (-(n • x)) = conj (fourier n x) := by
  rw [← neg_smul, ← fourier_apply]; exact fourier_neg

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