no goals
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = selfAdjoint.expUnitary b * selfAdjoint.expUnitary a
rw [← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]