OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootWeylFourier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier matrix row of the actual conjugated inversion on a global section. Its zero branch is retained separately from the finite cubic-character row.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_fourier_row line 13