OAI/GroupTheory/PolycyclicRecognition/Geometry/CentralRootGenerators.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite generation up to roots through a central extension

  1. theorem OAI.PolycyclicRecognition.exists_fg_subgroup_containing_powers_of_center line 13