TODO: Add doc-string.

theorem NumberField.Odlyzko.tsum_sigma_of_summable {β : Type u_1} {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [T3Space E] {γ : β → Type u_3} (w : (b : β) × γ b → E) (hfiber : ∀ (b : β), Summable fun (x : γ b) => w ⟨b, x⟩) (hw : Summable w) : ∑' (x : (b : β) × γ b), w x = ∑' (b : β) (x : γ b), w ⟨b, x⟩

theorem NumberField.Odlyzko.hasSum_inversePower_eq_lSeries_fiberCard {α : Type u_1} (ν : α → ℕ) [∀ (n : ℕ), Finite { a : α // ν a = n }] (hν : ∀ (a : α), ν a ≠ 0) {s : ℂ} (hsum : Summable fun (a : α) => ↑(ν a) ^ (-s)) : HasSum (fun (a : α) => ↑(ν a) ^ (-s)) (LSeries (fun (n : ℕ) => ↑(Nat.card { a : α // ν a = n })) s)

theorem NumberField.Odlyzko.summable_inversePower_of_lSeriesSummable_fiberCard {α : Type u_1} (ν : α → ℕ) [∀ (n : ℕ), Finite { a : α // ν a = n }] (hν : ∀ (a : α), ν a ≠ 0) {s : ℂ} (hsum : LSeriesSummable (fun (n : ℕ) => ↑(Nat.card { a : α // ν a = n })) s) : Summable fun (a : α) => ↑(ν a) ^ (-s)