DFinsupp Infinite not Finite

theorem DFinsuppInfinite_not_Finite : ¬(Module.Finite ℤ A) := by  /- Prove by giving a series of Module equivalences (LinearEquiv's) between DFinsupp,  Finsupp, and finally Polynomial, where we can appeal to Polynomial.not_finite to do the  lifting for us. -/  have f : (Polynomial ℤ) ≃ₗ[ℤ] (Finsupp ℕ ℤ) := {    toFun := Polynomial.toFinsupp    invFun := Polynomial.ofFinsupp    map_add' _ _ := by simp; rfl    map_smul' := by      intros      rw [zsmul_eq_mul, eq_intCast, Int.cast_id, ← zsmul_eq_mul]      rfl    left_inv := by simp [Function.LeftInverse]    right_inv := by simp [Function.RightInverse, Function.LeftInverse]  }  rw [← Module.Finite.equiv_iff (finsuppLequivDFinsupp ℤ), ← Module.Finite.equiv_iff f]  exact Polynomial.not_finite