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