OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual complex root element acts on the arithmetic subgroup with its original cubic multiplier.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootElement line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootElement_intertwines line 16