mathlib3

84f2e934 - feat(group_theory/free_abelian_group): add free_abelian_group.basis (#11465)

feat(group_theory/free_abelian_group): add free_abelian_group.basis (#11465) Although a statement about `free_abelian_group`, it lives in `free_abelian_group_finsupp` because it uses the isomorphism between `free_abelian_group X` and `X →₀ ℤ` Co-authored-by: Adam Topaz <github@adamtopaz.com>