OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteRationalLinearModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The rational linear quotient of a finite-dimensional solvable group

The vector space is the product of the rational upper central layers of an actual maximal nilpotent normal subgroup. Its action is faithful on the quotient. No finite generation of the nilpotent subgroup is assumed.

  1. structure OAI.PolycyclicRecognition.FiniteRationalLinearModel line 15
  2. theorem OAI.PolycyclicRecognition.exists_nilpotent_normal_rational_linear_quotient line 28