noncomputable def HexNumberFieldMathlib.Unity.zeta (n : ℕ) : ℂ

The standard positive primitive root of unity.

Equations

• HexNumberFieldMathlib.Unity.zeta n = Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)

theorem HexNumberFieldMathlib.Unity.primitive {n : ℕ} (hn : n ≠ 0) : IsPrimitiveRoot (zeta n) n

theorem HexNumberFieldMathlib.Unity.arg_zeta {n : ℕ} (hn : 2 < n) : (zeta n).arg = 2 * Real.pi / ↑n

theorem HexNumberFieldMathlib.Unity.im_zeta {n : ℕ} (hn : 2 < n) : 0 < (zeta n).im

theorem HexNumberFieldMathlib.Unity.arg_lower {n : ℕ} (hn : n ≠ 0) {w : ℂ} (hw : w ^ n = 1) (him : 0 < w.im) : 2 * Real.pi / ↑n ≤ w.arg

Positive arguments of nth roots of unity are at least one full turn divided by n.

theorem HexNumberFieldMathlib.Unity.eq_of_max {n : ℕ} (hn : 2 < n) {w : ℂ} (hw : w ^ n = 1) (him : 0 < w.im) (hre : (zeta n).re ≤ w.re) : w = zeta n

Maximal real part among upper roots selects the standard primitive root.