OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The root subgroup has central diagonal reduction modulo the prime. Its diagonal cubic character is therefore trivial.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_diagonal_square line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_diagonal_character line 19
  3. def OAI.CubicFirstMoment.cubicThetaPrimeRootDilationIwahori line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootDilation_kubota line 39