Zulip Chat Archive

Stream: Is there code for X?

Topic: compute degree and leading term


view this post on Zulip Anatole Dedecker (Dec 09 2020 at 14:43):

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

view this post on Zulip Patrick Massot (Dec 09 2020 at 14:44):

What are you assumptions on the base ring?

view this post on Zulip Patrick Massot (Dec 09 2020 at 14:45):

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 Z/3\mathbb{Z}/3.

view this post on Zulip Johan Commelin (Dec 09 2020 at 14:45):

@Patrick Massot you mean degree 0 and lc 1

view this post on Zulip Patrick Massot (Dec 09 2020 at 14:45):

Yes zero

view this post on Zulip Anatole Dedecker (Dec 09 2020 at 14:47):

Oh indeed, but in my case I'm working on R\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 :/

view this post on Zulip Patrick Massot (Dec 09 2020 at 14:48):

Maybe you are missing some simp lemmas then.

view this post on Zulip Riccardo Brasca (Dec 09 2020 at 14:56):

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.


Last updated: May 19 2021 at 02:10 UTC