Frobenius determinant theorem

frobenius_group_determinant

Submitter: Kim Morrison.

Notes: Dedekind's group determinant: the determinant of the group matrix A_{gh} = x_{gh} (over ℂ[x_g : g ∈ G]) factors into irreducible polynomials, each to the power of its own total degree, with factors pairwise non-associated and their number equal to the number of conjugacy classes of G. The helpers groupMatrix and groupDeterminant encode the statement; over ℂ this is the algebraically-closed characteristic-zero form where Frobenius's theorem and the character correspondence d_j = deg p_j live. Mathlib has MvPolynomial, Matrix.det, unique factorization, character theory, and ConjClasses, but not the group determinant or its factorization. Category-(b) candidate.

Source: Knill, *Some fundamental theorems in mathematics*, §171.

Informal solution: This is the genesis of representation theory. By Maschke and Wedderburn the group algebra ℂ[G] decomposes as a product of matrix algebras ⨁ⱼ M_{dⱼ}(ℂ), one per irreducible representation ρⱼ of dimension dⱼ. The group matrix is the matrix of left regular multiplication by the generic element ∑_g x_g g, so its determinant is the product over the regular-representation blocks, det = ∏ⱼ det(ρⱼ(∑_g x_g g))^{dⱼ}. Each factor pⱼ = det(ρⱼ(∑_g x_g g)) is an irreducible polynomial of total degree dⱼ, the factors are pairwise non-associated, and the number of irreducibles equals the number of conjugacy classes of G.

theorem declaration uses `sorry`frobenius_group_determinant (G : Type*) [Group G] [Fintype G] [DecidableEq G] :
    ∃ (r : ℕ) (p : Fin r → MvPolynomial G ℂ),
      r = Nat.card (ConjClasses G) ∧
      (∀ j, Irreducible (p j)) ∧
      (∀ i j, i ≠ j → ¬ Associated (p i) (p j)) ∧
      groupDeterminant G = ∏ j, (p j) ^ (p j).totalDegree := byG:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:DecidableEq G⊢ ∃ r p,
  r = Nat.card (ConjClasses G) ∧
    (∀ (j : Fin r), Irreducible (p j)) ∧
      (∀ (i j : Fin r), i ≠ j → ¬Associated (p i) (p j)) ∧ groupDeterminant G = ∏ j, p j ^ (p j).totalDegree
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 22, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 22, 2026