mathlib3

a33d01f7 - feat(analysis/inner_product_space/spectrum): add a decomposition instance (#14870)

feat(analysis/inner_product_space/spectrum): add a decomposition instance (#14870) This `decomposition` instances inherits the noncomputability of `orthogonal_projection`, but it is at least defeq to something useful.