OAI/GroupTheory/PolycyclicRecognition/Geometry/AbelianRootGenerators.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite generation up to roots in a finite-rank abelian group

  1. theorem OAI.PolycyclicRecognition.rationalAbelianMap_span line 13
  2. theorem OAI.PolycyclicRecognition.exists_finite_rationalAbelian_spanning_set line 27
  3. theorem OAI.PolycyclicRecognition.abelian_exists_fg_subgroup_containing_powers line 53