Eigenvalues of elements of prime order

DefinitionZalesskiĭ's problem on eigenvalues of elements of prime order (Kourovka 11.35)#✓fully proved

The statement that for every \(n\), every finite subgroup \(H\) of \(\mathrm{GL}_n(\mathbb{C})\) and every \(h \in H\) of prime order \(p\) that lies in no abelian normal subgroup of \(H\), the element \(h\) has at least \((p - 1)/2\) distinct eigenvalues, that is, \(p - 1 \le 2k\) where \(k\) is the number of distinct roots of the characteristic polynomial of \(h\).

def primeOrderElementManyEigenvalues : Prop :=
  ∀ (n : ℕ) (H : Subgroup (Matrix.GeneralLinearGroup (Fin n) ℂ)),
    (H : Set (Matrix.GeneralLinearGroup (Fin n) ℂ)).Finite → ∀ h ∈ H, (orderOf h).Prime →
    (∀ A : Subgroup (Matrix.GeneralLinearGroup (Fin n) ℂ), A ≤ H →
      (∀ x ∈ H, ∀ a ∈ A, x * a * x⁻¹ ∈ A) → (∀ a ∈ A, ∀ b ∈ A, a * b = b * a) → h ∉ A) →
    orderOf h - 1 ≤ 2 * (h : Matrix (Fin n) (Fin n) ℂ).charpoly.roots.toFinset.card

Used by 1

Used byRobinson's theorem on eigenvalues of elements of prime order

TheoremRobinson's theorem on eigenvalues of elements of prime order#●ready to prove

For every \(n\), if \(H\) is a finite subgroup of \(\mathrm{GL}_n(\mathbb{C})\) and \(h \in H\) has prime order \(p\) and lies in no abelian normal subgroup of \(H\), then \(h\) has at least \((p - 1)/2\) distinct eigenvalues, that is, \(p - 1 \le 2k\) where \(k\) is the number of distinct roots of the characteristic polynomial of \(h\). This answers Kourovka Notebook Problem 11.35 (A. E. Zalesskiĭ) in the affirmative.

public theorem_wanted primeOrderElementManyEigenvalues_holds : primeOrderElementManyEigenvalues

def primeOrderElementManyEigenvalues : Prop :=
  ∀ (n : ℕ) (H : Subgroup (Matrix.GeneralLinearGroup (Fin n) ℂ)),
    (H : Set (Matrix.GeneralLinearGroup (Fin n) ℂ)).Finite → ∀ h ∈ H, (orderOf h).Prime →
    (∀ A : Subgroup (Matrix.GeneralLinearGroup (Fin n) ℂ), A ≤ H →
      (∀ x ∈ H, ∀ a ∈ A, x * a * x⁻¹ ∈ A) → (∀ a ∈ A, ∀ b ∈ A, a * b = b * a) → h ∉ A) →
    orderOf h - 1 ≤ 2 * (h : Matrix (Fin n) (Fin n) ℂ).charpoly.roots.toFinset.card

WantedExt/GroupTheory/LinearGroupPrimeOrderEigenvaluesKourovka11Problem35Wanted.lean:43

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 11.35 (A. E. Zalesskiĭ); resolution: G. R. Robinson, J. Algebra 178, no. 2 (1995), 635-642, Kourovka Archive, Problem 11.35: "Yes, it is", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesZalesskiĭ's problem on eigenvalues of elements of prime order (Kourovka 11.35)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.