OAI/GroupTheory/PolycyclicRecognition/Algebra/NumberFieldTorsionLinearGroups.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Torsion linear groups over number fields

Restriction of scalars gives a faithful finite-dimensional rational action. This statement needs no finite-generation hypothesis on the group.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_of_faithful_numberField_torsion line 15