OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeDerivativeAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The derivative adjoint of the literal cubed-prime correspondence. It uses the same inversion conjugate as the mass adjoint.

  1. lemma OAI.CubicFirstMoment.cubicThetaPointC1_trace_atkin_section line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHecke_gradient_adjoint line 21