Theorem unitary.inv_mul_mem_iff

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

feat: `a * b⁻¹` for `a b : Aˣ` is unitary if `star a * a = star b * b` (#24858)