Expressing x⁻¹ from a polynomial equality

Stream: Is there code for X?

[Eric Wieser]

If I have a polynomial p = a + bx + cx² + dx³ + ⋯, do we have a definition that produces the polynomial -(b + cx + dx² + ⋯)/a?

That is, the expression you get from rearranging a + bx + cx² + dx³ + ⋯ = 0 to x⁻¹ = -(b + cx + dx²)/a?

I'm not familiar with the appropriate terminology here, so don't know what to look for.

[Eric Wieser]

Ah, docs#polynomial.div_X looks pretty close, I guess I'm asking for -p.div_X / p.coeff 0.

[Anne Baanen]

See also docs#inv_eq_of_aeval_div_X_ne_zero and further, where this is used to compute inverses in subalgebras of algebraic field extensions.

[Eric Wieser]

Indeed, I found that lemma after looking for places where div_X was used