OAI/NumberTheory/CubicMoment/Estimates/KummerChebyshevFromPrimitive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal cubic-symbol prime sum for every nonzero noncube numerator, from the primitive Hecke completion input and proved elementary reciprocity.

  1. theorem OAI.CubicFirstMoment.kummer_chebyshev_from_primitive line 12