mathlib

638dd0f8 - feat(data/dfinsupp, algebra/direct_sum/module): direct sum on fintype (#9664)

feat(data/dfinsupp, algebra/direct_sum/module): direct sum on fintype (#9664) Analogues for `dfinsupp`/`direct_sum` of definitions/lemmas such as `finsupp.equiv_fun_on_fintype`: a `dfinsupp`/`direct_sum` over a finite index set is canonically equivalent to `pi` over the same index set.