summable_conj

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.summable_conj

English

For any f : α → 𝕜, Summable (fun a => conj (f a)) L is equivalent to Summable f L.

Русский

Для любой f : α → 𝕜, ряд суммируемости conj(f) равен суммируемости f.

LaTeX

$$Summable (fun a => conj (f a)) L ⇔ Summable f L$$

Lean4

@[simp]
theorem summable_conj {f : α → 𝕜} : Summable (fun x => conj (f x)) L ↔ Summable f L :=
  summable_star_iff

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

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

Разделы

Аффилиация

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