OAI/NumberTheory/CubicMoment/Estimates/PrimitiveCubicPrimeEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The character and square analytic data in the sharp prime theorem are supplied by primitive Hecke completion for a cubic finite character. Conjugation preserves its conductor and supplies precisely its square.

  1. theorem OAI.CubicFirstMoment.primitive_cubic_prime_ideal_estimate line 13