OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowerRoots.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A split polynomial with distinct roots modulo p has no additional roots modulo a power of p. This is the uniqueness part needed in the nonsingular congruence count.

  1. def OAI.TwoPointCorrelations.halaszPrimePowerReduction line 12
  2. lemma OAI.TwoPointCorrelations.halasz_prime_power_unit_iff line 16
  3. theorem OAI.TwoPointCorrelations.halasz_prime_power_split_roots line 32