neg_iff

Mathlib.NumberTheory.LSeries.Linearity

URI: https://scilib.ai/kg/mathlib#LSeriesSummable.neg_iff

English

The negation of summability is equivalent: LSeriesSummable(-f) s ↔ LSeriesSummable f s.

Русский

Эквивалента суммируемости: LSeriesSummable(-f) s ↔ LSeriesSummable f s.

LaTeX

$$$$ \mathrm{LSeriesSummable}(-f,s) \iff \mathrm{LSeriesSummable}(f,s). $$$$

Lean4

@[simp]
theorem neg_iff {f : ℕ → ℂ} {s : ℂ} : LSeriesSummable (-f) s ↔ LSeriesSummable f s :=
  ⟨fun H ↦ neg_neg f ▸ H.neg, .neg⟩

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

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

Разделы

Аффилиация

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