module): use `decomposition` instead of `is_internal` when the equiv is needed
#14812

Open

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

eric-wieser wants to merge 5 commits into master from eric-wieser/more-is_internal

refactor(algebra/direct_sum/module): use `decomposition` instead of `…

e5221a1b

eric-wieser added awaiting-CI

fix

c5a0a4ed

add nonconstructive approach

5501d2c2

fix

fa3d72bf

eric-wieser added awaiting-review

rebuild the cache please

c783cc6b

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review awaiting-CI too-late

Milestone

No milestone