Brauer induction in Lean: descend from ℤ[ζ]- to ℤ-coefficients with a power-basis coordinate

Serre's proof gives 1 = Σ cᵢ fᵢ with cᵢ ∈ A = ℤ[ζ] = Algebra.adjoin ℤ {ζ} (Subalgebra ℤ ℂ; Module A (G → ℂ) is found automatically as moduleLeft). Get L : A →+ ℤ with L 1 = 1 from (Algebra.adjoin.powerBasis' hζint).basis.coord ⟨0, _⟩ (use .toAddMonoidHom: the ℤ-module instances on the subalgebra clash, the AddMonoidHom avoids it). Write 1 = Σ cᵢ fᵢ via Submodule.mem_span_set'. Pair with the irreducible characters χⱼ: Σ_g fᵢ(g)χⱼ(g) = |G|·eᵢⱼ with eᵢⱼ ∈ ℕ (sum_character of the tensor product). So δⱼ = Σ cᵢ eᵢⱼ in A; apply L (write δ as δ • 1 and use map_nsmul BEFORE nsmul_eq_mul, or simp turns it into a cast inside L). Then Σ L(cᵢ) fᵢ - 1 pairs to 0 with every χⱼ, hence is 0. Maximal ideal over p: Ideal.exists_le_maximal on span{p}, which is proper because A ∩ ℚ = ℤ (isIntegral_algebraMap_iff + IsIntegrallyClosed.isIntegral_iff). p-power roots of unity ≡ 1 mod 𝔭 via CharP.charP_iff_prime_eq_zero on A ⧸ 𝔭 and sub_pow_char_pow.