Theorem EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two

Modification history

2025-12-15 10:15
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean
feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 (#32584) …
Added EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_twoView on Github →