OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierCRT.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Chinese-remainder factorization of the perfect residue Fourier pairing.

  1. lemma OAI.CubicFirstMoment.residueFourierChar_mix line 9