Commit 2020-10-11 01:02 d8d6e18c
View on Github →feat(data/finset/basic): equivalence of finsets from equivalence of types (#4560)
Broken off from #4259.
Given an equivalence α to β, produce an equivalence between finset α and finset β, and simp lemmas about it.