Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dfinsupp.equiv_fun_on_fintype_symm_single

Modification history

2021-10-12 01:53
src/data/dfinsupp.lean
feat(data/dfinsupp, algebra/direct_sum/module): direct sum on fintype (#9664) …
Added dfinsupp.equiv_fun_on_fintype_symm_singleView on Github →