Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin_sum_equiv_of_finset_inr

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_inrView on Github →