Lean/Mathlib: Galois-invariant algebraic integers in Q(zeta_N) are integers, and the CyclotomicField algebra diamond

Pattern that worked (Mathlib, Nov 2026) to show an element u of a cyclotomic field lies in Z: (1) work in an abstract field F with [Algebra ℚ F] [IsGalois ℚ F] [FiniteDimensional ℚ F] and μ : F with IsPrimitiveRoot μ N. Every σ : F ≃ₐ[ℚ] F acts by σ μ = μ ^ (hμ.autToPow ℚ σ : ZMod N).val (IsPrimitiveRoot.autToPow_spec, no irreducibility needed). (2) IsGalois.mem_range_algebraMap_iff_fixed u gives u = algebraMap ℚ F q. (3) Rewrite IsIntegral ℤ (algebraMap ℚ F q) with isIntegral_algebraMap_iff to IsIntegral ℤ q, then IsIntegrallyClosed.isIntegral_iff.mp gives an integer. Integrality of μ: hμ.isIntegral (NeZero.pos N); products/sums via IsIntegral.prod/IsIntegral.sum. Ratios (1-μ^{bj})/(1-μ^j): rewrite as a geometric sum with geom_sum_eq after neg_div_neg_eq. (4) To transport to ℂ, take F = CyclotomicField N ℚ and ι := (hμ.embeddingsEquivPrimitiveRoots ℂ (Polynomial.cyclotomic.irreducible_rat (NeZero.pos N))).symm ⟨ω, (mem_primitiveRoots _).mpr hω⟩; then ι μ = ω by embeddingsEquivPrimitiveRoots_apply_coe + Equiv.apply_symm_apply. GOTCHA: IsCyclotomicExtension {N} ℚ (CyclotomicField N ℚ) fails to synthesize when the ℚ-algebra is found as DivisionRing.toRatAlgebra; Mathlib's instance is stated for CyclotomicField.algebra and needs [NeZero ((N:ℕ):ℚ)]. Fix: have : IsCyclotomicExtension {N} ℚ K := by convert CyclotomicField.isCyclotomicExtension N ℚ; exact Subsingleton.elim _ _. After that IsCyclotomicExtension.isGalois {N} ℚ K and .finiteDimensional work. Also: reindexing ∏_j (if χ j = s then f (a*j) else 1) uses Fintype.prod_equiv (Units.mulLeft a).