Solve `x^n = 1` in Complex

Stream: new members

[White Chen]

In lean 4, how to prove that $x=e^{\frac{2\pi k i}{n}}$, if $x^n=1$ ?
I formailize this as follow:

import Mathlib
open Complex Polynomial

noncomputable def p := fun (n : ℕ) => monomial n (1 : ℂ)

example {n : ℕ} : p n = 1
                  ↔ (p n).rootSet ℂ  = {x | ∀ k ∈ Finset.range n, x = exp (2*π*k*I / n)} := sorry

[Edward van de Meent]

i think the easiest way would be to first prove that $x=e^{\frac{2\pi ki}{n}}$ is a solution to the polynomial for all $0 \leq k < n$ and that these are all different, then show that there are at most $n$ solutions because that is the degree of the polynomial. from that you can conclude that the earlier solutions must be all of them

[Johan Commelin]

See also docs#Complex.isPrimitiveRoot_iff