isPrimitiveRoot_exp — Mathlib

English

The primitive root of unity given by the exponential function exp(2πi/n) is a primitive nth root of unity for n ≠ 0.

Русский

Примитивный корень единицы, заданный через экспоненту exp(2πi/n), является примитивным корнем порядка n при n ≠ 0.

LaTeX

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

Lean4

theorem isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (exp (2 * π * I / n)) n := by
  simpa only [Nat.cast_one, one_div] using isPrimitiveRoot_exp_of_coprime 1 n h0 n.coprime_one_left

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