mathlib

c21561a0 - feat(algebra/direct_sum): Reindexing direct sums (#13076)

feat(algebra/direct_sum): Reindexing direct sums (#13076) Lemmas to reindex direct sums, as well as to rewrite direct sums over an option or sigma type. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>