A valuation obstruction to roots of the rational-function variable

The variable X is not an n-th power in K(X) for n > 1: its order at infinity is -1, whereas the order of an n-th power is divisible by n. This supplies non-power coefficients for Laurent-series pole obstructions over rational function fields.

theorem TauCeti.ratFunc_pow_ne_X {K : Type u_1} [Field K] {n : ℕ} (hn : 1 < n) (b : RatFunc K) : b ^ n ≠ RatFunc.X

The rational-function variable is not an n-th power when n > 1.