theorem Hex.AlgebraicNumber.Radical.polynomial_value (a : AlgebraicNumber) {n : ℕ} (hn : n ≠ 0) : (polynomial a n).toPolynomial = Polynomial.X ^ n - Polynomial.C a.toComplex

The root solver receives exactly X^n - a.

theorem Hex.AlgebraicNumber.Radical.select_value (a : AlgebraicNumber) {n : ℕ} (hn : n ≠ 0) : ∃ (c : Candidate), select (polynomial a n).roots.toArray = some c ∧ c.value.toComplex = a.toComplex ^ (↑n)⁻¹

Selection succeeds and returns the principal complex root.

theorem Hex.AlgebraicNumber.Radical.fast?_value (a : AlgebraicNumber) {n : ℕ} (hn : 1 < n) (ha : a.toComplex ≠ 0) {out : AlgebraicRoot} (h : fast? a (polynomial a n).roots.toArray = some out) : out.toComplex = a.toComplex ^ (↑n)⁻¹

The lazy branch selector returns the same principal value as the exact reference.

@[simp]

theorem Hex.AlgebraicNumber.nthRoot_toComplex (a : AlgebraicNumber) (n : ℕ) : (a.nthRoot n).toComplex = a.toComplex ^ (↑n)⁻¹

The executable nth root agrees with Mathlib's principal complex power.

@[simp]

theorem Hex.AlgebraicNumber.nthRoot_pow (a : AlgebraicNumber) {n : ℕ} (hn : n ≠ 0) : a.nthRoot n ^ n = a

Every positive-index radical is a root of the expected equation.

@[simp]

theorem Hex.AlgebraicNumber.sqrt_toComplex (a : AlgebraicNumber) : a.sqrt.toComplex = a.toComplex.sqrt

The executable square root uses Mathlib's principal branch.

@[simp]

theorem Hex.AlgebraicNumber.sqrt_sq (a : AlgebraicNumber) : a.sqrt ^ 2 = a

theorem Hex.AlgebraicNumber.nthRoot_conj (a : AlgebraicNumber) (n : ℕ) (ha : a.toComplex.arg ≠ Real.pi) : a.conj.nthRoot n = (a.nthRoot n).conj

Conjugation commutes with the principal radical away from the negative-real branch cut.

theorem Hex.AlgebraicNumber.nthRoot_conj_of_not_lt (a : AlgebraicNumber) (n : ℕ) (ha : ¬a < 0) : a.conj.nthRoot n = (a.nthRoot n).conj

A decidable branch-cut condition for conjugating principal radicals.