OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrincipalTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The level-three determinant identity forces the trace to be 2 modulo 9. Together with the elliptic trace bound, this isolates trace 2 without an assumed torsion-freeness theorem.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrincipal_trace_mod_nine line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrincipal_trace_eq_two_of_norm_le line 25