OAI/NumberTheory/CubicMoment/Theta/CubicThetaUnitCharacterFourier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite additive frequency of the unit supplementary character.

  1. lemma OAI.CubicFirstMoment.cubicThetaAddChar_eq_of_generators line 9
  2. def OAI.CubicFirstMoment.cubicThetaUnitFourierCharacter line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaUnitFourierCharacter_apply line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaUnitCharacter_fourier line 39