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>

src/group_theory/free_abelian_group_finsupp.lean

@@ -6,6 +6,8 @@ Authors: Johan Commelin
 
 import group_theory.free_abelian_group
 import data.finsupp.basic
+import data.equiv.module
+import linear_algebra.dimension
 
 /-!
 # Isomorphism between `free_abelian_group X` and `X →₀ ℤ`
@@ -94,6 +96,11 @@ def equiv_finsupp : free_abelian_group X ≃+ (X →₀ ℤ) :=
   right_inv := to_finsupp_to_free_abelian_group,
   map_add' := to_finsupp.map_add }
 
+/-- `A` is a basis of the ℤ-module `free_abelian_group A`. -/
+noncomputable def basis (α : Type*) :
+  basis α ℤ (free_abelian_group α) :=
+⟨(free_abelian_group.equiv_finsupp α).to_int_linear_equiv ⟩
+
 variable {X}
 
 /-- `coeff x` is the additive group homomorphism `free_abelian_group X →+ ℤ`