Extending a dual family to a basis

For Proposition 7.5: in a free abelian group of finite rank, elements x_i admitting integer functionals h_j with h_j(x_i) = δ_ij are part of a basis (exists_basis_of_dual). The projection v ↦ ∑ h_i(v) x_i splits off the span of the x_i, with basis the x_i; its kernel is free, being finite and torsion-free.

theorem MultiplicativeBasisDeformations.exists_basis_of_dual {N : Type} [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] {n : ℕ} (x : Fin n → N) (h : Fin n → N →ₗ[ℤ] ℤ) (hd : ∀ (i j : Fin n), (h i) (x j) = if i = j then 1 else 0) : ∃ (ι : Type) (b : Module.Basis ι ℤ N) (j : Fin n → ι), Function.Injective j ∧ ∀ (i : Fin n), b (j i) = x i

A dual family is part of a basis.