mathlib3

feat(analysis/inner_product_space/trace_class): define the trace of a positive operator

#15451

Open