OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootTranslationIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

First-level Hilbert orthogonality, expressed as its literal fundamental-domain integral for finite-cover transport.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRoot_translation_integral_zero line 11