mathlib

ae10dced - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626)

feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626) This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`. The main user-facing changes are: * `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom` * The simp normal form of decomposition is now `direct_sum.decompose`. * `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support` * `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>