making an inverse to a bijection

Stream: new members

[Sebastian Zimmer]

Is there something in mathlib that lets you (constructively) make an inverse to a bijection between two fintypes with decidably equality?

It feels to me like it should be possible without axioms.

[Mario Carneiro]

You are right that it is possible without axioms, but I don't think we have exactly that

[Sebastian Zimmer]

How about unique choice in a fintype?

[Mario Carneiro]

There is encodable.choose, but a fintype isn't actually encodable because it doesn't have an ordering

[Mario Carneiro]

but as you say for unique choice it doesn't matter

[Mario Carneiro]

That's something that makes sense to define, but you would have to write it yourself (and PR to mathlib)

[Sebastian Zimmer]

I've implemented this. Should I make a PR to leanprover-community or directly to leanprover/mathlib?

[Bryan Gin-ge Chen]

You should PR directly to mathlib. leanprover-community is typically used as a collaborative staging area for larger PR's that multiple people work on; you can get contributor access to it if you ask Mario or Simon Hudon.

[Mario Carneiro]

I don't know your github username

[Bryan Gin-ge Chen]

It looks like Sebastian has already opened a PR to leanprover-community:

https://github.com/leanprover-community/mathlib/pull/7

[Sebastian Zimmer]

ok, I've opened a PR directly to mathlib here https://github.com/leanprover/mathlib/pull/421

[Sebastian Zimmer]

I made a bunch of changes in reponse to the comments on it