OAI/GroupTheory/PolycyclicRecognition/Algebra/InfiniteAbelianIntegerQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An integer quotient of an infinite finitely generated abelian group

We use the structure theorem only to select one free coordinate. The resulting map is an actual surjective group homomorphism to the integers.

  1. theorem OAI.PolycyclicRecognition.infinite_fg_abelian_integer_quotient line 14