OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteKernelAscendingData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite kernels above the ascending structural case

The full height, letter and stable base are lifted along the homomorphism. Thus a finite-by-ascending virtually nilpotent group satisfies the same finite-index solvable finite-dimension conclusion.

  1. def OAI.PolycyclicRecognition.AscendingVirtuallyNilpotentData.liftFiniteKernel line 17
  2. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_finiteKernel_ascending line 75