hasSum_conj' — Mathlib

English

The same statement as HasSum conj' but expressed via a different conjugation isomorphism: HasSum conj' f x L ↔ HasSum f x L.

Русский

Та же идея, что и HasSum conj', выраженная через другое сопряжение: HasSum conj' f x L ↔ HasSum f 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)) (conj x) L ↔ HasSum f x L :=
  RCLike.hasSum_conj' _

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