OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaMultiplication.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unrestricted arithmetic multiplication identity for the cubic Kubota value at level nine. The finite shear removes the auxiliary coprimality hypothesis from the direct reciprocity calculation.

  1. lemma OAI.CubicFirstMoment.primary_add_nine_mul line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaKubota_shear line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaKubota_product_nonzero line 31
  4. theorem OAI.CubicFirstMoment.cubicThetaKubota_product line 53

    Source documentation

    Arithmetic multiplication, including the zero lower-left entry.

    theorem cubicThetaKubota_product
    {a b c d e f : Eisenstein} (ha : primary a) (he : primary e)
    (hdet : a*d-b*c = 1) (hbf : (9:Eisenstein) ∣ b*f) (hef : IsCoprime e f) :
    cubicSymbol (a*e+b*f) (c*e+d*f) = cubicSymbol a c*cubicSymbol e f := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol