OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeConjugation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The integral prime correspondence on the actual level-three group. Conjugation has its exact cubic diagonal twist, including zero lower-left entries.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahori_division line 12
  2. def OAI.CubicFirstMoment.cubicThetaPrimeConjugatedMatrix line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeConjugatedMatrix_mem line 27
  4. def OAI.CubicFirstMoment.cubicThetaPrimeConjugate line 40
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeConjugate_kubota line 45