Theorems · Theorem · number theory

ModularForm.tsum_logDeriv_eta_q

∀ (z : ℂ),
  ∑' (n : ℕ), logDeriv (fun x => 1 - ModularForm.eta_q n x) z =
    2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), (↑n + 1) * -ModularForm.eta_q n z / (1 - ModularForm.eta_q n z)

Defined in: Mathlib.NumberTheory.ModularForms.DedekindEta
Cited by: 1 results in Mathlib
Foundations: Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Complexstatement and proof · cited by 5,565
SummationFilter.unconditionalstatement and proof · cited by 2,068
Real.pistatement and proof · cited by 1,774
Complex.ofRealstatement and proof · cited by 1,654
tsumstatement and proof · cited by 1,148
Complex.Istatement and proof · cited by 866
logDerivstatement · cited by 71
tsum_congrproof · cited by 64
tsum_mul_leftproof · cited by 21
ModularForm.eta_qstatement and proof · cited by 15

Cited by1

Results whose statement or proof uses this declaration.

ModularForm.logDeriv_eta_eq_E2proof · cited by 1