Finset.Icc error

Stream: new members

[Janitha]

Finset.Icc 1 97

gives me an error: failed to synthesize
Preorder ℂ

I want to write

(∑ k ∈ Finset.Icc 1 97, k * (Complex.I ^ k)) = 48 + 49 * Complex.I

Context ---> I'm trying to formalize a proof of:

example (n : ℕ) : (∑ k ∈ Finset.Icc 1 n, k * (Complex.I ^ k)) = 48 + 49 * Complex.I ↔ n = 97 := by sorry

[Yaël Dillies]

What if you do k ∈ Finset.Icc (1 : ℕ) 97?

[Janitha]

That worked. Thanks!