OAI/GroupTheory/PolycyclicRecognition/Algebra/FinitelyGeneratedLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generation lifts through a surjection

Only finitely many chosen lifts are needed. This does not assert that the whole inverse image of a finitely generated subgroup is finitely generated.

  1. theorem OAI.PolycyclicRecognition.fg_subgroup_map line 14
  2. theorem OAI.PolycyclicRecognition.exists_fg_subgroup_surjective line 20