OAI/NumberTheory/CubicMoment/Transform/MetaplecticScaleMellin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mellin transform in the scale of the literal completed sum. Both the cube-product scale and the coprimality Euler factor are retained.

  1. theorem OAI.CubicFirstMoment.metaplectic_scale_mellin line 14