theorem HexNumberFieldMathlib.PrincipalRoot.arg_root {z : ℂ} (hz : z ≠ 0) {n : ℕ} (hn : n ≠ 0) : (z ^ (↑n)⁻¹).arg = z.arg / ↑n

Principal roots divide the input argument by the positive index.

theorem HexNumberFieldMathlib.PrincipalRoot.im_pos {z : ℂ} (hz : z ≠ 0) (hlo : 0 < z.arg) (hhi : z.arg < Real.pi) : 0 < z.im

A positive argument strictly below pi lies in the upper half plane.

theorem HexNumberFieldMathlib.PrincipalRoot.sector {z : ℂ} (hz : z ≠ 0) {n : ℕ} (hn : n ≠ 0) : -(Real.pi / ↑n) < (z ^ (↑n)⁻¹).arg ∧ (z ^ (↑n)⁻¹).arg ≤ Real.pi / ↑n

The principal radical has argument in the expected half-open sector.

theorem HexNumberFieldMathlib.PrincipalRoot.abs_arg_le {w v : ℂ} (hw : w ≠ 0) (hv : v ≠ 0) (hnorm : ‖w‖ = ‖v‖) (hre : v.re ≤ w.re) : |w.arg| ≤ |v.arg|

On a circle, greater real part means smaller absolute argument.

theorem HexNumberFieldMathlib.PrincipalRoot.eq_of_re {z w : ℂ} {n : ℕ} (hn : n ≠ 0) (hw : w ^ n = z) (hre : (z ^ (↑n)⁻¹).re ≤ w.re) (him : (z ^ (↑n)⁻¹).re = w.re → 0 ≤ (z ^ (↑n)⁻¹).im → 0 ≤ w.im) : w = z ^ (↑n)⁻¹

Maximal real part, with the nonnegative imaginary side preferred on a tie, selects exactly Mathlib's principal nth root.

theorem HexNumberFieldMathlib.PrincipalRoot.eq_of_max {z w : ℂ} {n : ℕ} (hn : n ≠ 0) (hw : w ^ n = z) (hre : ∀ (v : ℂ), v ^ n = z → v.re ≤ w.re) (him : ∀ (v : ℂ), v ^ n = z → v.re = w.re → 0 ≤ v.im → 0 ≤ w.im) : w = z ^ (↑n)⁻¹

Maximal real part and the upper tie select the principal root.