Traces in inner product spaces

This file contains various results about traces of linear operators in inner product spaces.

theorem LinearMap.trace_eq_sum_inner {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) (b : OrthonormalBasis ι 𝕜 E) : (trace 𝕜 E) T = ∑ i : ι, inner 𝕜 (b i) (T (b i))