OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDoubleRootConjugation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integral conjugation at the square root scale. The cubic twist of the dilation is trivial, so the original multiplier is retained exactly.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootIwahori line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRoot_lower_single_division line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootConjugate_dilation line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRoot_diagonal_character line 59
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootDilation_kubota line 65
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootConjugate_kubota line 76