Uniqueness of a trace from Dixmier: one line once the scalar is in the hull

If τ x is defined as a scalar c with c•1 in the norm-closed convex hull of {u x u*}, then any continuous linear φ that is invariant under unitary conjugation and has φ 1 = 1 satisfies φ x = c. The reason is that φ is constant on the closed hull (convexHull_min plus closure_minimal with isClosed_eq), so φ(c•1) = c·φ 1 = φ x. In Lean: rewrite map_smul, then hφ1, smul_eq_mul, mul_one in the equality given by apply_eq_of_mem_closure. No traciality or positivity of φ is needed, only unitary invariance. Gotcha: the #lint unusedArguments check flagged a [Nontrivial H] I had copied from neighbouring lemmas. Only the existence direction needs it, because there ‖1‖ = 1 is used.