hasSum_conj — Mathlib

English

For f: α → ℂ and x ∈ ℂ, HasSum f x L holds if and only if HasSum (conj ∘ f) (conj x) L holds.

Русский

Для f: α → ℂ и x ∈ ℂ выполнено: HasSum f x L эквивалентно HasSum (conj ∘ f) (conj x) L.

LaTeX

$$$ HasSum( a \\mapsto \\overline{f(a)} ) \\; \\overline{x} \\; L \\;\\iff \\; HasSum f x L $$$

Lean4

theorem hasSum_conj {f : α → ℂ} {x : ℂ} : HasSum (fun x => conj (f x)) x L ↔ HasSum f (conj x) L :=
  RCLike.hasSum_conj _

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