# Zulip Chat Archive

## Stream: new members

### Topic: polynomial: .to_fun vs .coeff

#### Damiano Testa (Sep 24 2020 at 11:30):

Dear All,

another question with a complete, yet annoying, proof. Lean likes to use `.to_fun`

to refer to the coefficients of a polynomial, but whenever it does, I need to insert a `have`

statement to convert `.to_fun`

to `.coeff`

(with proof `refl`

), since most of the functionality that I know uses `.coeff`

instead of `.to_fun`

. In the example below, you can see this happening at the `have`

line. Can I avoid the `have`

statement?

Thank you very much!

```
import tactic
import data.polynomial.degree.basic
open finset polynomial
lemma support_monomial {R : Type*} [semiring R] {n : ℕ} : (X ^ n : polynomial R).support ⊆ singleton n :=
begin
intros a a_1,
rw mem_singleton,
rw (X ^ n).3 at a_1,
have : (X ^ n).to_fun a = (X ^ n).coeff a,
refl,
rw this at a_1,
rw coeff_X_pow n a at a_1,
finish,
end
```

#### Kevin Buzzard (Sep 24 2020 at 11:32):

Things like `rw (X^n).3`

are not an official part of the API, which is why you're seeing `to_fun`

.

#### Damiano Testa (Sep 24 2020 at 11:33):

Ok, in this case, possibly. I have also seen it happen after `simp`

, though

#### Kevin Buzzard (Sep 24 2020 at 11:33):

```
lemma support_monomial {R : Type*} [semiring R] {n : ℕ} :
(X ^ n : polynomial R).support ⊆ singleton n :=
begin
intros a ha,
rw mem_singleton,
rw mem_support_iff_coeff_ne_zero at ha,
rw coeff_X_pow n a at ha,
finish,
end
```

#### Kevin Buzzard (Sep 24 2020 at 11:33):

If it happens after `simp`

then there might be a missing (or bad) simp lemma.

#### Damiano Testa (Sep 24 2020 at 11:34):

@Kevin Buzzard Thank you for the working example! This is what I was hoping for!

#### Damiano Testa (Sep 24 2020 at 11:35):

Kevin Buzzard said:

If it happens after

`simp`

then there might be a missing (or bad) simp lemma.

Should it happen again with `simp`

, I may report it as well

#### Kevin Buzzard (Sep 24 2020 at 11:36):

The trick with these things is to try and keep everything (hypotheses, goals) in the "standard form" (because this is what `simp`

and `rw`

like to see).

#### Scott Morrison (Sep 24 2020 at 12:23):

Essentially: anytime you see `.to_fun`

, it's a reflection that the API for polynomials is imperfect. We should aim to get out of this situation! The fact that `polynomial`

is actually defined in terms of `finsupp`

should be sealed away as early as practically possible. PRs that improve on this are very welcome. :-)

#### Damiano Testa (Sep 24 2020 at 12:25):

Very well: I will take a close look at whether I produce `.to_fun`

myself, or whether it is produced by `simp`

/Lean!

Last updated: May 14 2021 at 13:24 UTC