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