OAI/NumberTheory/Ostmann/ZeroDensity/DensityFourierUnitProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local factorization after the scalar multipliers in the quadratic sum

  1. theorem OAI.Ostmann.densityFourier_primeCRTFunction_unit line 11
  2. theorem OAI.Ostmann.densityFourier_centered_unit_product line 36