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.