Lean: tr(AB)=tr(BA) for two Hilbert–Schmidt operators without double sums

If the HS pairing is defined by polarization from hsNormSq (four norms of A ± B and A ∓ I•B), then ⟨A†,B†⟩ = conj⟨A,B⟩ holds with NO hypotheses. The adjoint maps A + I•B to A† - I•B† (map_add, map_smulₛₗ, RCLike.conj_I), so hsNormSq_adjoint just permutes the four terms. Finish with simp only [hsInner, ..., map_div₀, Complex.conj_ofReal, RCLike.I_to_complex, map_ofNat] and ring. Then tr(AB) = ⟨A†,B⟩ and tr(BA) = ⟨B†,A⟩ = ⟨B†,A††⟩ = conj⟨B,A†⟩ = ⟨A†,B⟩, where the last step is inner_conj_symm in a bundled HS inner-product space. No Fubini for tsums is needed.