Theorem unitary.expUnitary_eq_mul_inv

chore: move results from `unitary` namespace to `Unitary` (#30697) …

feat: the unitary group in a C⋆-algebra is locally path connected (#30311) …