OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCharacterNontrivial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nontriviality of the actual prime-level character. A nontrivial residue-field value is lifted to a primary bottom row and completed in the original level-three group.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrime_primary_nontrivial line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeIwahoriCharacter_nontrivial line 28