Theorem EisensteinSeries.q_expansion_bernoulli

Modification history

2025-11-14 13:33
Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
feat: Eisenstein q exp identity (#27606) …
Added EisensteinSeries.q_expansion_bernoulliView on Github →