MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryOddPrimePowerRoots

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_isUnit_of_reduction_ne_zero (p k : ℕ) [Fact (Nat.Prime p)] (hk : 1 ≤ k) (x : ZMod (p ^ k)) (hx : (ZMod.castHom ⋯ (ZMod p)) x ≠ 0) :

IsUnit x

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_isUnit_of_reduction_ne_zero · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_intCast_isUnit (p k : ℕ) [Fact (Nat.Prime p)] (a : ℤ) (ha : ¬↑p ∣ a) :

IsUnit ↑a

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_intCast_isUnit · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_sq_eq_sq (p k : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hk : 1 ≤ k) (u v : ZMod (p ^ k)) (hu : IsUnit u) (he : u ^ 2 = v ^ 2) :

u = v ∨ u = -v

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_sq_eq_sq · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_quadratic_root_card_le_two (p k : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hk : 1 ≤ k) (a d : ZMod (p ^ k)) (ha : IsUnit a) (hd : IsUnit d) :

{u : ZMod (p ^ k) | a * u ^ 2 = d}.card ≤ 2

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_quadratic_root_card_le_two · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_even_power_norm_le (p r : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hr : 1 ≤ r) (a d : ℤ) (ha : ¬↑p ∣ a) (hd : ¬↑p ∣ d) :

‖completeKloosterman (p ^ r * p ^ r) (↑a) d‖ ≤ 2 * ↑p ^ r

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_odd_even_power_norm_le · compiled type and proof/definition references.