OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianRankDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite integral dimension for countable torsion-free abelian groups

The rank bound is used on finitely generated subgroups. Each is an actual integral lattice, and the countable-union argument adds at most one dimension.

  1. theorem OAI.PolycyclicRecognition.abelian_fg_subgroup_lattice_of_rank line 19
  2. theorem OAI.PolycyclicRecognition.abelian_fg_subgroup_dimension_of_rank line 37
  3. theorem OAI.PolycyclicRecognition.abelian_cohomologicalDimension_of_rank line 45