Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 23:11 2153dc34

View on Github →

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

Estimated changes

Modified src/data/fintype/sort.lean

added def fin_sum_equiv_of_finset

added theorem fin_sum_equiv_of_finset_inl

added theorem fin_sum_equiv_of_finset_inr