Theorem summable_finset_prod_of_summable_norm

Modification history

2026-04-26 16:26
Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
chore: camel-case `finset_sum` in lemma names (#37793) …
Deleted summable_finset_prod_of_summable_normView on Github →
2026-03-31 07:42
Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …
Added summable_finset_prod_of_summable_normView on Github →