Elementary quadratic Gauss cancellation by translation and additive orthogonality. The linear coefficient is unrestricted; no multiplicative character is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_quadratic_gauss_norm (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (A B : ZMod p) (hA : A ≠ 0) : ‖∑ x : ZMod p, ZMod.stdAddChar (A * x ^ 2 + B * x)‖ = √↑p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_sum_reduction (q r : ℕ) [NeZero q] [NeZero r] (F : ZMod q → ℂ) : ∑ x : ZMod (q * r), F ((ZMod.castHom ⋯ (ZMod q)) x) = ↑r * ∑ y : ZMod q, F y

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_isUnit_add_cube_zero {q : ℕ} (u t : ZMod q) (ht : t ^ 3 = 0) : IsUnit (u + t) ↔ IsUnit u

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_inv_add_cube_zero {q : ℕ} (u t : ZMod q) (hu : IsUnit u) (ht : t ^ 3 = 0) : (u + t)⁻¹ = u⁻¹ - t * u⁻¹ ^ 2 + t ^ 2 * u⁻¹ ^ 3