## Stream: Is there code for X?

### Topic: compute degree and leading term

#### 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

#### Patrick Massot (Dec 09 2020 at 14:44):

What are you assumptions on the base ring?

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

#### Johan Commelin (Dec 09 2020 at 14:45):

@Patrick Massot you mean degree 0 and lc 1

Yes zero

#### Anatole Dedecker (Dec 09 2020 at 14:47):

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 (Dec 09 2020 at 14:48):

Maybe you are missing some simp lemmas then.

#### 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