compute degree and leading term

Stream: Is there code for X?

[Anatole Dedecker]

Is there any simple way to prove that an explicitely given polynomial (like 3*X^2 - 6*X + 7) has a given degree or leading_coeff ? simp doesn't want to do it

[Patrick Massot]

What are you assumptions on the base ring?

[Patrick Massot]

The answer very much depends on it. Do you expect the degree to be 1 and leading coefficient to be 1 in your example? Because this is what happens over $\mathbb{Z}/3$.

[Johan Commelin]

@Patrick Massot you mean degree 0 and lc 1

[Patrick Massot]

Yes zero

[Anatole Dedecker]

Oh indeed, but in my case I'm working on $\mathbb{R}$. To give a bit of context I've proven some lemmas about limits of ratios of polynomials, and I wanted to see if it made proving a particular limit easier. But I get stuck on proving degrees and leading coeffs like that, which is annoying :/

[Patrick Massot]

Maybe you are missing some simp lemmas then.

[Riccardo Brasca]

You can see in data.polynomial.degree.definitions. It's not very quick, but for monimials there are lemmas that say what you want (both the degree and the leading coefficient), then you can use lemmas like polynomial.degree_add_eq_left_of_degree_lt and polynomial.leading_coeff_add_of_degree_lt.