Theorem Int.cast_complex_isTheta_cast_real

Modification history

2025-06-26 13:35
Mathlib/Analysis/Complex/Asymptotics.lean
feat: Add more Summability results needed for Eisenstein series. (#26005) …
Added Int.cast_complex_isTheta_cast_realView on Github →