English
Under ExpChar p, ζ ∈ rootsOfUnity(p^k·m) R iff ζ ∈ rootsOfUnity(m) R.
Русский
При ExpChar p верно ζ ∈ корни(p^k·m) эквивалентно ζ ∈ корни(m).
LaTeX
$$$\zeta \in rootsOfUnity(p^k \cdot m)\;R \iff \zeta \in rootsOfUnity(m)\;R$$$
Lean4
/-- The complex `n`-th roots of unity are exactly the
complex numbers of the form `exp (2 * Real.pi * Complex.I * (i / n))` for some `i < n`. -/
nonrec theorem mem_rootsOfUnity (n : ℕ) [NeZero n] (x : Units ℂ) :
x ∈ rootsOfUnity n ℂ ↔ ∃ i < n, exp (2 * π * I * (i / n)) = x :=
by
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]
have hn0 : (n : ℂ) ≠ 0 := mod_cast NeZero.out
constructor
· intro h
obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x := by
simpa only using (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h
refine ⟨i, hi, ?_⟩
rw [← H, ← exp_nat_mul]
congr 1
field_simp
· rintro ⟨i, _, H⟩
rw [← H, ← exp_nat_mul, exp_eq_one_iff]
use i
simp [field]
