Lean/Mathlib: classify real primitive Dirichlet characters via CRT components and x^2 = 0

To split χ : DirichletCharacter ℂ (m*n) with m ⊥ n, define the components as MulChars by a ↦ χ((ZMod.chineseRemainder h).symm (a, 1)) and b ↦ χ(symm (1, b)). map_one' is rw [Prod.mk_one_one, map_one, map_one], and map_nonunit' uses hu.map (chineseRemainder h) with Prod.isUnit_iff. Primitivity of a component follows from the witness form (a k coprime to the level with k ≡ 1 mod d and χ k ≠ 1) applied at d*n. To kill a real character on the kernel of p^(j+2) → p^(j+1), set x = p^(j+1) t in ZMod: x*x = 0 and p*x = 0, so (1+x)^p = 1 + p x = 1 (a two-line induction). For 2^(j+4) use 1 + 2^(j+3) t ≡ (1 + 2^(j+2) t)^2, which ring checks on ℕ. Gotchas: case-split N = 2^k q with rcases k first, then have : N = q * 4; subst so the levels are syntactically q*4. not_isUnit_zero on ZMod 4 needs have : Fact (1 < 4). In the k = 1 branch of Nat.recOnPosPrimePosCoprime, rw [pow_one] the ∀-goal before intro.