Real-angle integer phase character on the complex unit circle

import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

set_option autoImplicit false

noncomputable section

namespace WindingArithmeticDensePhase

/-- The point of the complex unit circle obtained by rotating through the
integer multiple `n * α` of a real angle. -/
noncomputable def realCirclePhase (α : ℝ) (n : ℤ) : Circle :=
  Circle.exp ((n : ℝ) * α)

/-- Integer addition represented as multiplication of real-angle phases. -/
noncomputable def realCircleCharacter (α : ℝ) : AddChar ℤ Circle where
  toFun := realCirclePhase α
  map_zero_eq_one' := by simp [realCirclePhase]
  map_add_eq_mul' m n := by
    simp only [realCirclePhase]
    rw [show (((m + n : ℤ) : ℝ) * α) =
      (m : ℝ) * α + (n : ℝ) * α by push_cast; ring]
    exact Circle.exp_add _ _

end WindingArithmeticDensePhase