OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootBruhatMatrix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An integral Bruhat representative for two inverse nonzero root parameters. Its multiplier is the literal cubic residue symbol.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootBruhat_division line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeRootBruhatMatrix line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootBruhatMatrix_mem line 23
  4. def OAI.CubicFirstMoment.cubicThetaPrimeRootBruhat line 35
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootBruhat_kubota line 39