Commit 2026-01-22 10:30 e43baf02

View on Github →

feat(NumberTheory/ModularForms/Basic): Provide definition of the products of finitely many modular forms (#32978) finprod_equal_weights: the product of n modular forms of weight k is a modular form of weight n * k finprod_add_weights: the product of n modular forms of different weights has weight the sum of the weights

Estimated changes