Complex.mem_rootsOfUnity
theorem Complex.mem_rootsOfUnity :
∀ (n : ℕ+) (x : ℂˣ), x ∈ rootsOfUnity n ℂ ↔ ∃ i < ↑n, (2 * ↑Real.pi * Complex.I * (↑i / ↑↑n)).exp = ↑x
The theorem `Complex.mem_rootsOfUnity` asserts that for any positive integer `n` and any nonzero complex number `x`, `x` is an `n`-th root of unity if and only if there exists an integer `i` such that `i` is less than `n` and `x` equals `exp (2 * π * i * I / n)`. Here, `exp` denotes the exponential function, `π` is the mathematical constant Pi, `I` is the imaginary unit, and `/ n` means division by `n`. In other words, this theorem establishes exactly which complex numbers are the `n`-th roots of unity, in terms of their exponential form involving `i`, `π`, and `n`.
More concisely: For a positive integer n and a nonzero complex number x, x is an n-th root of unity if and only if there exists an integer i < n such that x = exp(2πiI/n).
|
Complex.isPrimitiveRoot_exp
theorem Complex.isPrimitiveRoot_exp : ∀ (n : ℕ), n ≠ 0 → IsPrimitiveRoot (2 * ↑Real.pi * Complex.I / ↑n).exp n := by
sorry
This theorem, `Complex.isPrimitiveRoot_exp`, states that for any natural number `n` that is not zero, the complex number obtained as the result of the complex exponential function applied to `(2 * pi * i / n)` is a primitive nth root of unity. Here, `pi` refers to the mathematical constant Pi, `i` is the imaginary unit, and the complex exponential function is defined via its Taylor series. A primitive nth root of unity is a complex number whose nth power equals 1 and that is not a kth power of any other complex number for any positive integer k smaller than n. The notation `Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)` represents the complex exponential function applied to the complex number `(2 * pi * i / n)`. The arrow `↑` is the coercion operator in Lean, which allows for the conversion between types — in this case, from real numbers to complex numbers.
More concisely: For any natural number $n \neq 0$, the complex number $\exp\left(\frac{2\pi i}{n}\right)$ is a primitive $n$th root of unity.
|