mathlib

e5221a1b - refactor(algebra/direct_sum/module): use `decomposition` instead of `is_internal` when the equiv is needed