hasSum_conj'

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.hasSum_conj'

English

For any f : α → 𝕜 and x ∈ 𝕜, HasSum (fun a => conj (f a)) (conj x) L iff HasSum f x L.

Русский

Для любой f : α → 𝕜 и x ∈ 𝕜, HasSum(conj f) (conj x) L ⇔ HasSum f x L.

LaTeX

$$HasSum (fun a => conj (f a)) (conj x) L ⇔ HasSum f x L$$

Lean4

theorem hasSum_conj' {f : α → 𝕜} {x : 𝕜} : HasSum (fun x => conj (f x)) (conj x) L ↔ HasSum f x L :=
  conjCLE.hasSum'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru