Character Degree Divisibility

Abstract

Finite representation theory relates simple modules, characters, conjugation and induction.

Theorem 1.1 (Trace eq finrank iff).

$$\forall V\in Type\ast ,[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(\mathrm{Complex},V\right)],[\mathrm{FiniteDimensional}\left(\mathrm{Complex},V\right)],\forall f\in \mathrm{Module}.\mathrm{End}\left(\mathrm{Complex},V\right),\forall n\in \mathrm{Nat},(\mathrm{Ne}\left(n,0\right))\Rightarrow (((\mathrm{HPow}.\mathrm{hPow}\left(f,n\right))=(1))\Rightarrow (((\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearMap}.\mathrm{trace}\left(\mathrm{Complex},V\right),f\right))=(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},V\right)\right)))\iff ((f)=(1))))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CharacterDegreeDivisibility.trace_eq_finrank_iff (✓ std3). ∎

Citation. The Tau Ceti contributors; Claude (2026). TauCeti finite representation and character theory. URL: https://github.com/TauCetiProject/TauCeti/tree/a780c7ad6beb23f60a17351a492d177878020ad5.

Commentary.

The displayed conclusion holds under the stated hypotheses.

Theorem 1.2 (Finrank dvd card).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{Finite}\left(G\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{CharZero}\left(k\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],\mathrm{Dvd}.\mathrm{dvd}\left(\mathrm{Module}.\mathrm{finrank}\left(k,V\right),\mathrm{Nat}.\mathrm{card}\left(G\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CharacterDegreeDivisibility.finrank_dvd_card (✓ std3). ∎

Citation. The Tau Ceti contributors; Claude (2026). TauCeti finite representation and character theory. URL: https://github.com/TauCetiProject/TauCeti/tree/a780c7ad6beb23f60a17351a492d177878020ad5.

Commentary.

The displayed conclusion holds under the stated hypotheses.

References

• Truth anchor: D5/S3/FiniteGroups/CharacterDegreeDivisibility.finrank_dvd_card
• Truth anchor: D5/S3/FiniteGroups/CharacterDegreeDivisibility.trace_eq_finrank_iff
• Dependency: D5/S3/FiniteGroups/FiniteCharacterAlgebra