OAI/NumberTheory/CubicMoment/Theta/CubicThetaLevelAngular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All nonzero signed angular transformations at primary-level rational cusps, derived from the actual automorphic theta function by small-circle extraction.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmetic_level_angular line 16