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

[ADedecker]

---

• depends on: [Merged by Bors] - refactor(analysis/inner_product_space/pi_L2): change std_orthonormal_basis to type orthonormal_basis #12253
• depends on: [Merged by Bors] - feat(analysis/inner_product_space/positive): definition and basic facts about positive operators #15470
• depends on: [Merged by Bors] - feat(analysis/normed_space/linear_isometry): linear_equiv.of_eq as a linear_isometry_equiv #15471
• depends on: [Merged by Bors] - feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span #15481
• depends on: [Merged by Bors] - feat(analysis/inner_product_space/[pi_L2, l2_space]): compute inner product in a given [orthonormal, hilbert] basis #15514
• depends on: [Merged by Bors] - feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis #15540
• depends on: [Merged by Bors] - feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U #15541
• depends on: [Merged by Bors] - feat(analysis/inner_product_space/basic): orthonormal version of linear_independent.coe_range #15577
• depends on: [Merged by Bors] - feat(analysis/normed_space/operator_norm): variant of continuous_linear_equiv.has_sum #15578

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(analysis/inner_product_space/pi_L2): change std_orthonormal_basis to type orthonormal_basis #12253
• [Merged by Bors] - feat(analysis/inner_product_space/positive): definition and basic facts about positive operators #15470
• [Merged by Bors] - feat(analysis/normed_space/linear_isometry): linear_equiv.of_eq as a linear_isometry_equiv #15471
• [Merged by Bors] - feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span #15481
• [Merged by Bors] - feat(analysis/inner_product_space/[pi_L2, l2_space]): compute inner product in a given [orthonormal, hilbert] basis #15514
• [Merged by Bors] - feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis #15540
• [Merged by Bors] - feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U #15541
• [Merged by Bors] - feat(analysis/inner_product_space/basic): orthonormal version of linear_independent.coe_range #15577
• [Merged by Bors] - feat(analysis/normed_space/operator_norm): variant of continuous_linear_equiv.has_sum #15578
  By Dependent Issues (🤖). Happy coding!