Twisted Chinese remaindering for the actual complete Kloosterman sum

The two twists are the integer Bezout coefficients: m * gcdA m n + n * gcdB m n = 1. Thus gcdB m n is the inverse of n modulo m. No frequency is required to be a unit, and either coprime factor may be one. These are exact arithmetic identities, not an invocation of a Weil bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stdAddChar_mul_modulus (q r : ℕ) [NeZero q] [NeZero r] (z : ℤ) : ZMod.stdAddChar (↑r * ↑z) = ZMod.stdAddChar ↑z

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_map_inv_of_isUnit {q r : ℕ} (f : ZMod q →+* ZMod r) {u : ZMod q} (hu : IsUnit u) : f u⁻¹ = (f u)⁻¹

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stdAddChar_crt (m n : ℕ) [NeZero m] [NeZero n] (h : m.Coprime n) (z : ZMod (m * n)) : ZMod.stdAddChar z = ZMod.stdAddChar (↑(m.gcdB n) * ((ZMod.chineseRemainder h) z).1) * ZMod.stdAddChar (↑(m.gcdA n) * ((ZMod.chineseRemainder h) z).2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_crt (m n : ℕ) [NeZero m] [NeZero n] (h : m.Coprime n) (a d : ℤ) : completeKloosterman (m * n) (↑a) d = completeKloosterman m (↑(a * m.gcdB n)) (d * m.gcdB n) * completeKloosterman n (↑(a * m.gcdA n)) (d * m.gcdA n)

Multiplicativity with both frequencies twisted by the opposite modulus's inverse.