OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeIwahori.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-index subgroup and cubic diagonal character needed for the unramified local correspondence. All data come from reduction of the principal arithmetic group; no local representation input is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeIwahori line 14
  2. def OAI.CubicFirstMoment.cubicThetaPrimeReduction line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeReduction_ker_le line 32
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeIwahori_finiteIndex line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahori_diagonal_coprime line 46
  6. def OAI.CubicFirstMoment.cubicThetaPrimeIwahoriCharacter line 53
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahoriCharacter_norm line 67
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahoriCharacter_cube line 71