## Stream: new members

### Topic: Function from {0,1...,n-1}

#### Riccardo Brasca (Sep 29 2020 at 13:45):

Hi all. I would like to tell Lean that I have a function $f \colon \{0,1,\ldots, n -1\}$, but I do not know how to represent it. My first attempt was to define a function f : finset.range n \to \C, but then I realize that finset.range n has type finset \N, so it is not a Type and I do not know I to define functions from it.

Maybe it is the wrong way of thinking, my situation is the following. I have an function $f \colon \mathbf{N} \to \mathbf{C}$, whose restriction to the set $\{0,\ldots n-1\}$ is injective but $f$ is not . I can of course write down that if $x,y \in \mathbf{N}$ are such that $x,y < n$ and $f(x)=f(y)$ then $x=y$, but it seems more natural to me to have some function g such that g.injective holds. Thank you!

#### Sebastien Gouezel (Sep 29 2020 at 13:47):

You can say something like injective (λ (i : fin n), f i) (untested)

#### Riccardo Brasca (Sep 29 2020 at 13:48):

@Sebastien Gouezel Thank you! fin n was the type I was looking for!

#### Reid Barton (Sep 29 2020 at 14:11):

For what it's worth, we also have docs#set.inj_on

#### Johan Commelin (Sep 29 2020 at 15:07):

@Riccardo Brasca I just made a PR on (primitive/complex) roots of unity: #4260

#### Riccardo Brasca (Sep 29 2020 at 15:10):

@Johan Commelin Thank you! I will have a look at it... it is probably (better then) what I was writing at the moment :grinning:

Last updated: May 12 2021 at 04:19 UTC