A basis of a finite abelian group

By the structure theorem a finite abelian group is a product of cyclic groups. Read through the generators of the factors, this says that a finite abelian group G has a finite family of elements σ i that generates it and whose orders multiply to |G| (CommGroup.exists_closure_range_eq_top_and_prod_orderOf_eq_card). The product formula is what distinguishes such a basis from an arbitrary finite generating family, whose orders multiply to a multiple of |G|; it is the input to determinant arguments over the group ring of G, where the order of each basis element appears as a diagonal entry.

theorem CommGroup.exists_closure_range_eq_top_and_prod_orderOf_eq_card (G : Type u_1) [CommGroup G] [Finite G] : ∃ (ι : Type) (x : Fintype ι) (σ : ι → G), Subgroup.closure (Set.range σ) = ⊤ ∧ ∏ i : ι, orderOf (σ i) = Nat.card G

A finite abelian group has a basis: a finite generating family whose orders multiply to the order of the group.