# Zulip Chat Archive

## Stream: new members

### Topic: fintype to finset

#### Eloi (Jul 17 2020 at 21:56):

Is it possible to convert a `fintype`

to a `finset`

and later recover the fintype?

I'm trying to define Theta series of a quadratic form, and I need `fin 2`

... but the `∑`

notation requires a finset...

```
noncomputable def Theta'(z: ℂ)(Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
cau_seq ℂ complex.abs :=
⟨λ M, ∑ m in finset.pi (fin 2) (λ n, Ico_ℤ (- M) M), exp(2 * pi * I * z * (Q m)), sorry⟩
```

#### Jalex Stark (Jul 17 2020 at 22:00):

you might like to use `\sum m in finset.range 2`

#### Jalex Stark (Jul 17 2020 at 22:01):

I'm not sure what you mean by recover

#### Eloi (Jul 17 2020 at 22:04):

Then to define a sum over ℤ² I need a sum inside a sum, right?

I mean that `m`

is indexed by a `finset`

, but a quadratic form has to be applied to a term of type `fin 2 → ℤ`

To be clear, my dream would be to be able to write something like

```
∑ m in (fin 2 → Ico_ℤ (- M) M)
```

#### Jalex Stark (Jul 17 2020 at 22:11):

oh I misunderstood your code

#### Jalex Stark (Jul 17 2020 at 22:12):

I usually either use a double sum or index over the product type

#### Jalex Stark (Jul 17 2020 at 22:14):

can you post code that compiles? I'm not familiar with the parts of the library you're using, so chasing down the imports is not fun

#### Eloi (Jul 17 2020 at 22:29):

sure, I updated the first comment to make this thread more readable :)

#### Alex J. Best (Jul 17 2020 at 23:20):

```
import data.complex.basic
import data.real.pi
import linear_algebra.quadratic_form
open real -- pi
open complex
open finset -- Ico_ℤ
open cau_seq
open_locale big_operators
variable M : ℕ
noncomputable def Theta'(z: ℂ) (Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
cau_seq ℂ complex.abs :=
⟨λ M, ∑ m in finset.pi (univ : finset (fin 2)) (λ n, Ico_ℤ (- M) M), exp (2 * (real.pi : ℂ) * I * z * (Q (λ t, m t (mem_univ t)))), sorry⟩
```

#### Alex J. Best (Jul 17 2020 at 23:27):

actually using `fintype.pi_finset`

instead seems nicer

```
noncomputable def Theta'(z: ℂ) (Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
cau_seq ℂ complex.abs :=
⟨λ M, ∑ m in fintype.pi_finset (λ a : fin 2, Ico_ℤ (- M) M), exp (2 * (real.pi : ℂ) * I * z * Q m), sorry⟩
```

and if I were you I think I'd separate the creation of the theta series into making a power series in `q`

with integer coefficients, and then evaluation as a complex function!

#### Eloi (Jul 18 2020 at 05:33):

Nice! Thank you, I'll do so

Last updated: May 13 2021 at 05:21 UTC