OAI/GroupTheory/PolycyclicRecognition/Algebra/SchurTorsionLinearGroups.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Schur's finiteness theorem for characteristic-zero linear groups

A finitely generated torsion group with a faithful finite-dimensional characteristic-zero matrix representation is finite. The coefficient field, the uniform eigenvalue-degree bound, and the common exponent are constructed.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_of_faithful_fg_torsion line 16
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.infinite_fg_linear_group_has_infinite_order line 25