OAI/NumberTheory/CubicMoment/Theta/CubicThetaUnitPhaseSymbol.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact matching of the unit phase and supplementary symbol in the ramified arithmetic theta coefficient.

  1. lemma OAI.CubicFirstMoment.cubicThetaNinePhase_congr line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaNinePhase_omega line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaNinePhase_omega_square line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaUnitPhase_neg line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaUnitPhase_omega_power line 38
  6. theorem OAI.CubicFirstMoment.cubicThetaUnitPhase_eq line 63
  7. lemma OAI.CubicFirstMoment.cubicThetaUnit_square_congruence line 77
  8. theorem OAI.CubicFirstMoment.cubicThetaNinePhase_unit_primary line 90