isPrimitiveRoot_exp_of_coprime — Mathlib

English

For coprime i, n with n ≠ 0, the complex exponential e^{2πi i/n} is a primitive nth root of unity.

Русский

Для сравнительно простых i и n, n ≠ 0, число e^{2πi i/n} является примитивным корнем единицы порядка n.

LaTeX

$$$\text{IsPrimitiveRoot}(e^{2\pi i i/n}, n)$$$

Lean4

theorem isPrimitiveRoot_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.Coprime n) :
    IsPrimitiveRoot (exp (2 * π * I * (i / n))) n :=
  by
  rw [IsPrimitiveRoot.iff_def]
  simp only [← exp_nat_mul, exp_eq_one_iff]
  constructor
  · use i
    simp (discharger := norm_cast) [field]
  · simp only [forall_exists_index]
    have hn0 : (n : ℂ) ≠ 0 := mod_cast h0
    rintro l k hk
    field_simp at hk
    norm_cast at hk
    have : n ∣ l * i := by rw [← Int.natCast_dvd_natCast, hk]; apply dvd_mul_right
    exact hi.symm.dvd_of_dvd_mul_right this

Похожие утверждения