McKay conjecture on character degrees

### What is the conjecture

The McKay conjecture is a statement about the relationship between the character degrees of a finite group and those of the normalizer of its Sylow subgroups.

Let $G$ be a finite group, let $\ell$ be a prime, and let $P$ be a Sylow $\ell$-subgroup of $G$. Denote by $\text{Irr}(G)$ the set of irreducible complex characters of $G$. The **McKay conjecture** states:

$$|\{\chi \in \text{Irr}(G) : \gcd(\chi(1), \ell) = 1\}| = |\{\psi \in \text{Irr}(N_G(P)) : \gcd(\psi(1), \ell) = 1\}|$$

where $N_G(P)$ denotes the normalizer of $P$ in $G$, and $\chi(1)$ is the degree (dimension) of the character $\chi$. The conjecture asserts that the number of irreducible characters of $G$ with degree coprime to $\ell$ equals the number of irreducible characters of $N_G(P)$ with degree coprime to $\ell$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/McKay_conjecture, https://arxiv.org/abs/2410.20392, https://annals.math.princeton.edu/articles/22056

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-03-14)

Building blocks (from Mathlib):
- `Sylow p G`: Sylow p-subgroups (Mathlib.GroupTheory.Sylow)
- `Subgroup.normalizer`: subgroup normalizers (Mathlib.GroupTheory.Subgroup)
- Character theory basics: character of representations, orthogonality results (Mathlib.RepresentationTheory.Character)

Missing pieces (not found in Mathlib search):
- Classification of irreducible characters of finite groups by degree
- Systematic theory of character degrees and their divisibility properties
- Connection between character degrees of a group and normalizers of Sylow subgroups

Rating justification: Sylow subgroups and basic character theory exist in Mathlib, but the conjecture requires significant additional infrastructure around character degree theory, including definitions of character degree as an irreducible character property and lemmas relating character degrees across subgroups. The statement itself can be formalized once character degree infrastructure is developed, estimated at moderate complexity.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)