OAI/NumberTheory/CubicMoment/Theta/CubicThetaBaseScalarSign.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The only remaining normalization ambiguity is the sign of the actual base coefficient. No choice of that sign is made here.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticBaseScalar_sq line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticBaseScalar_sign line 20