Commit 2020-06-30 04:15 38904ac8

feat(data/fintype/basic): card_eq_zero_equiv_equiv_pempty (#3238) Adds a constructive equivalence α ≃ pempty.{v+1} given fintype.card α = 0, which I think wasn't available previously. I would have stated this as an iff, but as the right hand side is data is an equiv itself.