OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootBruhatResidues.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Choice-independent nonzero Bruhat branches, indexed by the actual prime residue units. The cubic multiplier is the original residue character.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootReciprocal line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_nine_unit line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootReciprocal_pair line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootBruhat_residue_character line 36
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_residue_branch line 43