Lean: tr(ST) = tr(TS) for trace-class T via unitary span, no double sums

Once the trace is basis-independent (HasSum (⟪eᵢ, T eᵢ⟫) (trace T) for every HilbertBasis), cyclicity is cheap. (1) Unitary invariance: transport the basis with HilbertBasis.ofRepr (e.symm.trans b.repr) for e = Unitary.linearIsometryEquiv U. Its apply lemma is two ← HilbertBasis.repr_symm_single rewrites plus rfl. Then ⟪U eᵢ, X U eᵢ⟫ = ⟪eᵢ, U†XU eᵢ⟫ by ← adjoint_inner_right, and HasSum.unique gives tr(U†XU) = tr X. (2) T U = U†(U T)U. (3) Extend to every S with Submodule.span_induction on CStarAlgebra.span_unitary : span ℂ (unitary A) = ⊤, using the ideal property and linearity of the trace. The zero case is just rw [zero_mul, mul_zero]. Gotcha: write coercions explicitly, as in X * (U : H →L[ℂ] H); X * U with U : unitary _ makes HMul synthesis time out.