Commit 2021-08-25 18:32 aca0874a
View on Github →chore(algebra/direct_sum): Move all the algebraic structure on direct_sum into a single directory (#8771)
This ends up splitting one file in two, but all the contents are just moved.
chore(algebra/direct_sum): Move all the algebraic structure on direct_sum into a single directory (#8771)
This ends up splitting one file in two, but all the contents are just moved.