OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootConjugation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootIwahori line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_lower_single_division line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootConjugate_dilation line 27
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootConjugate_kubota line 59