Zulip Chat Archive

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 ⁣:{0,1,,n1}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 ⁣:NCf \colon \mathbf{N} \to \mathbf{C}, whose restriction to the set {0,n1}\{0,\ldots n-1\} is injective but ff is not . I can of course write down that if x,yNx,y \in \mathbf{N} are such that x,y<nx,y < n and f(x)=f(y)f(x)=f(y) then x=yx=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: Dec 20 2023 at 11:08 UTC