Theorem EisensteinSeries.linear_isTheta_right

Modification history

2026-07-15 16:59
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted EisensteinSeries.linear_isTheta_rightView on Github →
2026-01-18 15:55
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
fix: add missing deprecations (#34087) …
Added EisensteinSeries.linear_isTheta_rightView on Github →
2025-12-27 18:03
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) …
Deleted EisensteinSeries.linear_isTheta_rightView on Github →
2025-06-26 13:35
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
feat: Add more Summability results needed for Eisenstein series. (#26005) …
Added EisensteinSeries.linear_isTheta_rightView on Github →