OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedCharacter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The supplementary character on primary elements modulo nine is an additive character of their two integral coordinates.

  1. def OAI.CubicFirstMoment.cubicThetaRamifiedCharacter line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRamifiedCharacter_one line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaRamifiedCharacter_omega line 29
  4. theorem OAI.CubicFirstMoment.cubicThetaRamifiedCharacter_coordinates line 32
  5. theorem OAI.CubicFirstMoment.cubicSymbol_lambda_primary_coordinates line 45