Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-02 01:20 73377021

View on Github →

feat(data/equiv/fintype): computable bijections and perms from/to fintype (#6959) Using exhaustive search, we can upgrade embeddings from fintypes into equivs, and transport perms across embeddings. The computational performance is poor, so the docstring suggests alternatives when an explicit inverse is known.

Estimated changes