# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: A vector range

#### Bolton Bailey (Dec 02 2020 at 22:58):

Is there code for a vector range analogous to the list.range function? If not, should this be added to vector.lean?

```
/-- Vector form of range function -/
def vector_range (k : ℕ) : vector ℕ k :=
⟨list.range k, by simp⟩
```

#### Yakov Pechersky (Dec 02 2020 at 23:05):

It doesn't currently. I've played around with it for quite some bit. What do you plan to do with it? I've found that working in lists usually ended up being easier.

#### Bolton Bailey (Dec 02 2020 at 23:30):

This function was useful for me when I wanted to represent a vector of powers of a polynomial variable, which I do using the expression

`def powers_of_τ : vector (mv_polynomial vars F) m := vector.map (λ i, X_poly^i) (vector_range m)`

In this case I want to use vector rather than list because later I want to take the dot product of this vector with another vector of polynomials, which I do using `vector.map₂`

with `*`

and then calling `to_list`

and `sum`

. I suppose I could convert everything to lists and use `list.map₂`

, but this seems less clean and I think I would later need to prove that these two lists are the same length. This actually raises another point: Is there code for taking the dot product of vectors of ring elements?

#### Yakov Pechersky (Dec 02 2020 at 23:31):

Might be easier to do this in `fin n \to R`

#### Yakov Pechersky (Dec 02 2020 at 23:32):

Because if you're going to reason about sum, it's going to be some unwieldy thing about `foldr`

or something like it, and you'll be juggling lemmas about associativity and identity elements. In `fin n \to R`

, you can use all the existing `big_operators`

lemmas about fintypes and fin.

#### Bolton Bailey (Dec 03 2020 at 10:02):

That sounds great. What are are these `big_operators`

you are talking about? `big_operators`

does not come up in a search of the lean documentation.

#### Reid Barton (Dec 03 2020 at 10:04):

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

Last updated: May 16 2021 at 05:21 UTC