OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootMatrix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integral formulas for conjugation by the fractional upper root 3x/p. The defining congruences give actual integral quotients.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_lower_division line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_diagonal_division line 16
  3. def OAI.CubicFirstMoment.cubicThetaPrimeRootMatrix line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootMatrix_mem line 39
  5. def OAI.CubicFirstMoment.cubicThetaPrimeRootConjugate line 60