OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowerCongruences.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Triangular systems of univariate polynomials reduce to power sums. The leading coefficients need only be units, so the result applies to the translated and differenced systems over prime-power residue rings.

  1. theorem OAI.TwoPointCorrelations.halasz_power_sums_of_polynomial_sums line 12
  2. theorem OAI.TwoPointCorrelations.halasz_prime_power_polynomial_count line 48