The rank of a free abelian group

A finitely generated free abelian group M is generated by the vectors of a ℤ-basis, so its minimal number of generators AddGroup.rank M is at most finrank ℤ M. This bounds the number of generators of a quotient of a lattice, such as the discriminant group of a full lattice.

Main statements

• AddGroup.rank_le_finrank: AddGroup.rank M ≤ finrank ℤ M for a finitely generated free abelian group M.

theorem AddGroup.rank_le_finrank (M : Type u_1) [AddCommGroup M] [FG M] [Module.Free ℤ M] : rank M ≤ Module.finrank ℤ M

A finitely generated free abelian group is generated by finrank ℤ M elements, the vectors of a basis.