OAI/GroupTheory/PolycyclicRecognition/Algebra/TorsionFreeAbelianRank.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform rank bounds on finitely generated abelian subgroups

A torsion-free finitely generated abelian group is an integral lattice. The explicit lattice duality calculation therefore bounds the rank of every such subgroup by a common ambient cohomological-dimension bound.

  1. def OAI.PolycyclicRecognition.integralLatticeEquivOfBasis line 21
  2. theorem OAI.PolycyclicRecognition.exists_integralLattice_equiv line 35
  3. theorem OAI.PolycyclicRecognition.abelian_subgroup_lattice_rank_bound line 52