feat(data/complex/circle): circle is a Lie group (#6907)
Define `circle` to be the unit circle in `ℂ` and give it the structure of a Lie group. Also define `exp_map_circle` to be the natural map `λ t, exp (t * I)` from `ℝ` to `circle`, and give it (separately) the structures of a group homomorphism and a smooth map (we seem not to have the definition of a Lie group homomorphism).
