HexNumberFieldMathlib.Unity

source

theorem Hex.AlgebraicNumber.Unity.polynomial_value (n : ℕ) :

HexRootsMathlib.toPolyℂ (polynomial n) = if n % 2 = 0 then Polynomial.X ^ (n / 2) + 1 else Polynomial.X ^ n - 1

The executable binomial has the stated complex interpretation.

source

theorem Hex.AlgebraicNumber.Unity.polynomial_ne_zero {n : ℕ} (hn : 2 < n) :

polynomial n ≠ 0

source

theorem Hex.AlgebraicNumber.Unity.zeta_mem {n : ℕ} (hn : 2 < n) :

(HexRootsMathlib.toPolyℂ (polynomial n)).IsRoot (HexNumberFieldMathlib.Unity.zeta n)

source

theorem Hex.AlgebraicNumber.Unity.root_pow {n : ℕ} (_hn : 2 < n) {z : ℂ} (hz : (HexRootsMathlib.toPolyℂ (polynomial n)).IsRoot z) :

z ^ n = 1

source

theorem Hex.AlgebraicNumber.Unity.generator?_value (n : ℕ) :

∃ (a : AlgebraicNumber), generator? n = some a ∧ a.toComplex = HexNumberFieldMathlib.Unity.zeta n

Construction of the primitive generator is total and chooses the standard branch.

source

@[simp]

theorem Hex.AlgebraicNumber.Unity.generator_toComplex (n : ℕ) :

(generator n).toComplex = HexNumberFieldMathlib.Unity.zeta n

source

@[simp]

theorem Hex.AlgebraicNumber.Unity.power_toComplex (a : AlgebraicNumber) (k : ℕ) :

(power a k).toComplex = a.toComplex ^ k

A fixed-field power has the same value as an ordinary algebraic power.

source

theorem Hex.AlgebraicNumber.Unity.turn_power (q : ℚ) :

HexNumberFieldMathlib.Unity.zeta q.den ^ (q.num % ↑q.den).toNat = Complex.exp (2 * ↑Real.pi * Complex.I * ↑q)

Reduction of the rational angle modulo one preserves the complex exponential.

source

@[simp]

theorem Hex.AlgebraicNumber.rootOfUnity_toComplex (q : ℚ) :

(rootOfUnity q).toComplex = Complex.exp (2 * ↑Real.pi * Complex.I * ↑q)

Rational turns agree exactly with Mathlib's complex exponential.

source

theorem Hex.AlgebraicNumber.rootOfUnity_primitive (q : ℚ) :

IsPrimitiveRoot (rootOfUnity q) q.den

The reduced denominator is the exact multiplicative order.

source

@[simp]

theorem Hex.AlgebraicNumber.rootOfUnity_zero :

rootOfUnity 0 = 1

source

@[simp]

theorem Hex.AlgebraicNumber.rootOfUnity_add (q r : ℚ) :

rootOfUnity (q + r) = rootOfUnity q * rootOfUnity r

source

@[simp]

theorem Hex.AlgebraicNumber.rootOfUnity_neg (q : ℚ) :

rootOfUnity (-q) = (rootOfUnity q).conj