# Zulip Chat Archive

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

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

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