OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full residue-unit diagonal quotient of the prime arithmetic subgroup. Surjectivity is proved by completing primary primitive rows.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeIwahoriDiagonal line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahoriDiagonal_coe line 28
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeIwahoriDiagonal_surjective line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeIwahoriCharacter_diagonal line 66