OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeResidueObstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The critical local image condition is exactly the two missing unramified residue identities. Neither identity is assumed here.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalGauss_ne_zero line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeResidueVector_line_iff_cube line 18
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeResidueImage_iff_identities line 43