Theorem Multipliable.tprod_pow

Modification history

2026-03-06 23:58
Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
feat(ModularForm/NumberTheory/Delta): Define the delta function (#34881) …
Added Multipliable.tprod_powView on Github →