Binomial equations over the Puiseux field

This file computes the roots of the binomials Y ^ n - a t ^ (n * q) in the Puiseux field puiseuxField K whenever K contains a primitive n-th root of unity: they are the monomials ζ ^ i b t ^ q with b ^ n = a. This covers the roots ζ ^ i t ^ (1 / n) of Y ^ n - t, whose leading order 1 / n is fractional, and the branches t ± t ^ (3 / 2) of (Y - t) ^ 2 = t ^ 3, which share the initial term t.

Main results

• TauCeti.puiseuxField.pow_eq_single_iff: the solutions of y ^ n = a t ^ (n * q).
• TauCeti.puiseuxField.pow_eq_single_one_iff: the solutions of y ^ n = t.
• TauCeti.puiseuxField.sub_single_sq_eq_single_iff: the solutions of (y - t) ^ 2 = t ^ 3.

theorem TauCeti.puiseuxField.pow_eq_single_iff {K : Type u_1} [Field K] {n : ℕ} (hn : 0 < n) {ζ : K} (hζ : IsPrimitiveRoot ζ n) (q : ℚ) (b : K) {y : ↥(puiseuxField K)} : y ^ n = single K (↑n * q) (b ^ n) ↔ ∃ i < n, y = single K q (ζ ^ i * b)

If K contains a primitive n-th root of unity ζ and b ^ n = a, then the solutions of y ^ n = a t ^ (n * q) in the Puiseux field are the monomials ζ ^ i b t ^ q for i < n.

theorem TauCeti.puiseuxField.pow_eq_single_one_iff {K : Type u_1} [Field K] {n : ℕ} (hn : 0 < n) {ζ : K} (hζ : IsPrimitiveRoot ζ n) {y : ↥(puiseuxField K)} : y ^ n = single K 1 1 ↔ ∃ i < n, y = single K (1 / ↑n) (ζ ^ i)

If K contains a primitive n-th root of unity ζ, then the roots of Y ^ n - t in the Puiseux field are the monomials ζ ^ i t ^ (1 / n) for i < n.

theorem TauCeti.puiseuxField.sub_single_sq_eq_single_iff {K : Type u_1} [Field K] {y : ↥(puiseuxField K)} : (y - single K 1 1) ^ 2 = single K 3 1 ↔ y = single K 1 1 + single K (3 / 2) 1 ∨ y = single K 1 1 - single K (3 / 2) 1

The solutions of (Y - t) ^ 2 = t ^ 3 in the Puiseux field are the branches t ± t ^ (3 / 2), which share the initial term t.