Lean/Mathlib: Montgomery's large sieve inequality via ZMod, only injectivity of the CRT map

For T(q) = sum over units b of ZMod q of |sum_n a_n stdAddChar(b*(M+n))|^2, the multiplicativity T(qp) >= w/(p-w) T(q) needs no Chinese remainder equivalence. Map (b1, b2) -> ((b1.val*p + b2.val*q : N) : ZMod (q*p)). Injectivity: apply ZMod.castHom (dvd_mul_right q p) and cancel the unit (p : ZMod q) (ZMod.isUnit_iff_coprime). Unit-ness: ZMod.isUnit_iff_coprime plus Nat.Coprime.mul_right. Then sum_image and sum_le_sum_of_subset_of_nonneg; surjectivity is never needed for a lower bound. The exponential identity is cleanest via ZMod.stdAddChar_coe on integer casts: stdAddChar((k : ZMod Q) * (j : ZMod Q)) = cexp(2 pi I k j / Q). Gotchas: DirichletCharacter has a Fintype instance without NeZero q, so sums over q in Icc 1 Q are fine, but stdAddChar needs NeZero (add have : NeZero q := ... per term). filter IsPrimitive needs open scoped Classical in. In the prime case, Lean's x/0 = 0 means w = p needs no separate hypothesis.