Mathlib v3 is deprecated. Go to Mathlib v4

Def fin_sum_equiv_of_finset

Modification history

2021-02-02 23:11

src/data/fintype/sort.lean

feat(data/fintype/sort): add `fin_sum_equiv_of_finset` (#6008)

Added fin_sum_equiv_of_finset View on Github →