feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators

feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators #20066