Lean/Mathlib: Gauss sums and root numbers of products of Dirichlet characters

For χ₁ mod m and χ₂ mod n with m ⊥ n, define the product as changeLevel (dvd_mul_right m n) χ₁ * changeLevel (dvd_mul_left n m) χ₂. Key value lemma: prod (k : ZMod (mn)) = χ₁ k * χ₂ k for every natural k. If k ⊥ mn, use DirichletCharacter.changeLevel_eq_cast_of_dvd' with IsCoprime (k:ℤ) (mn). Otherwise both sides vanish: use MulChar.map_nonunit, ZMod.isUnit_iff_coprime and Nat.coprime_mul_iff_right. Then reindex with x = a·n + b·m to get τ(prod) = χ₁(n)χ₂(m)τ₁τ₂. Primitivity criterion with natural witnesses: χ is primitive if for every proper d ∣ N there is k ⊥ N with k ≡ 1 [MOD d] and χ k ≠ 1. To extract a witness from a primitive χ, rewrite factorsThrough_iff_ker_unitsMap and IsConcreteLE.not_le_iff_exists (SetLike.not_le_iff_exists is deprecated). Split d as gcd(d,m)·gcd(d,n) with Nat.Coprime.gcd_mul, and combine the congruences with Nat.modEq_and_modEq_iff_modEq_mul. Sums over ZMod 4 or ZMod 8: change ∑ a : Fin 4, ... times out at whnf. Instead go through a lemma ∑ x : ZMod N, f x.val = ∑ r : Fin N, f r (prove it after obtain ⟨n, rfl⟩ : N = n+1, then rfl), and use Fin.sum_univ_eight. Character values come from decide on a list lookup.