OAI/GroupTheory/PolycyclicRecognition/Algebra/ClassTwoFiniteDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Class-two groups of finite rational abelianization rank

The central exterior bracket bounds the derived layer. Finite root cores in that layer and the abelianization then lift to an actual root core in the group. Torsion-free countable groups consequently have finite integral cohomological dimension.

  1. theorem OAI.PolycyclicRecognition.classTwo_rootCore_of_finite_abelianization line 21
  2. theorem OAI.PolycyclicRecognition.classTwo_finiteDimension_of_finite_abelianization line 33