Function from {0,1...,n-1}

Stream: new members

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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

[Reid Barton]

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

[Johan Commelin]

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

[Riccardo Brasca]

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