mathlib

73377021 - feat(data/equiv/fintype): computable bijections and perms from/to fintype (#6959)

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. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>