Theorem Real.prod_one_add_le_exp_sum

Modification history

2026-03-31 07:42
Mathlib/Analysis/Complex/Exponential.lean
feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …
Added Real.prod_one_add_le_exp_sumView on Github →