Commit 2021-10-12 01:53 638dd0f8

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.