periodic_expMapCircle

theorem periodic_expMapCircle : Function.Periodic (⇑expMapCircle) (2 * Real.pi)

The theorem `periodic_expMapCircle` states that the function `expMapCircle`, which maps a real number `t` to the unit circle in the complex plane via the expression `exp(t * I)`, is periodic. The period of this function is `2 * Real.pi`, i.e., twice the mathematical constant π. In other words, for all real numbers `t`, the value of `expMapCircle` at `t + 2π` is the same as its value at `t`.

More concisely: The complex function `exp(z => t * I)` (where `I` is the imaginary unit and `t` is a real number), denoted `expMapCircle`, is a periodic function with period `2 * Real.pi`.