Character values of finite groups lie in cyclotomic fields

brauer_character_in_cyclotomic

Submitter: Kim Morrison.

Notes: For a finite group G of exponent n, every value of every complex character of G lies in (the image of) the cyclotomic field ℚ(ζₙ). Stated uniformly for the fixed group G: there is a ring embedding φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ whose range contains tr(ρ(g)) for every finite-dimensional complex representation ρ of G and every g. This is a corollary of Brauer's induction theorem; the full splitting-field statement (every irreducible representation has a ℚ(ζₙ)-form) is strictly stronger and requires more scalar-extension scaffolding than mathlib currently exposes cleanly.

Source: R. Brauer, On the representation of a group of order g in the field of g-th roots of unity, Amer. J. Math. 67 (1945).

Informal solution: Choose an embedding φ : ℚ(ζₙ) ↪ ℂ once and for all for the fixed group G. Then apply Brauer's induction theorem uniformly: every complex character of G is a ℤ-combination of characters induced from elementary subgroups, and those induced character values lie in φ(ℚ(ζₙ)). Hence for every finite-dimensional complex representation ρ of G and every g ∈ G, tr(ρ(g)) lies in φ.range.

theorem declaration uses `sorry`brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] :
    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
        (ρ : Representation ℂ G V) (g : G),
        LinearMap.trace ℂ V (ρ g) ∈ φ.range := byG:Typeinst✝¹:Group Ginst✝:Fintype G⊢ ∃ φ,
  ∀ (V : Type) (x : AddCommGroup V) (x_1 : Module ℂ V),
    FiniteDimensional ℂ V → ∀ (ρ : Representation ℂ G V) (g : G), (LinearMap.trace ℂ V) (ρ g) ∈ φ.range
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 4, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 7, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 8, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 18, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026