Polynomial coefficient

Stream: Is there code for X?

[Gareth Ma]

Is there a direct lemma / theorem for this?

example {a : ℤ} {k : ℕ} : coeff (X ^ k * C a) k = a := by rw [coeff_mul_C, coeff_X_pow_self, one_mul]

exact? and simp? doesn't find it. More specifically

/- works -/
example {a : ℤ} {k : ℕ} : coeff (X ^ k * C a) k = a := by rw [coeff_mul_C, coeff_X_pow_self, one_mul]
/- doesn't -/
example {a : ℤ} {k : ℕ} : coeff (X ^ k * C a) k = a := by exact?
/- doesn't -/
example {a : ℤ} {k : ℕ} : coeff (X ^ k * C a) k = a := by simp?
/- works (but returns a suboptimal result) -/
example {k : ℕ} : coeff (X ^ k) k = 1 := by simp?
/- works -/
example {k : ℕ} : coeff (X ^ k) k = 1 := by rw [coeff_X_pow_self]

[Alex J. Best]

probably not. There is a lot of possible variants of such lemmas, so we tend to not add all possibilities, so if you state the lemma in a non-canonical way (i.e the coefficient after the power of X) I wouldn't expect to find many lemmas at all

[Alex J. Best]

your #mwe doesn't really work btw

[Alex J. Best]

Also what is suboptimal about the output of simp?

[Alex J. Best]

Actually maybe I shouldn't be so pessimistic, there is a lemma docs#Polynomial.coeff_mul_C, but a confluence issue stops it from firing, so simp [-eq_intCast] works for your first example

[Gareth Ma]

Oh, I didn't know about that - syntax. So it excludes a lemma?

[Alex J. Best]

Yes, in this case I noticed that simp? was telling me that all simp did was change the C a to a coercion of a, which seems unhelpful here, so I changed simp to exclude it.

[Gareth Ma]

I see. Also it keeps trying to use coeff_X_pow instead of coeff_X_pow_self. I wonder if the source code can be changed to prioritise the second

[Gareth Ma]

obviously it's more direct when applicable

[Alex J. Best]

coeff_X_pow_self isn't actually a simp lemma though. We could do what you suggest, but I'm not sure there will really be an appreciable difference in the end

[Gareth Ma]

Ah I see, nevermind then. Thanks for the help!

[Alex J. Best]

I'll make a PR adding

@[simp]
lemma coeff_mul_natCast {R : Type*} [Semiring R] {p : R[X]} {a : ℕ} : coeff (p * (a : R[X])) k = coeff p k * (↑a : R) := Polynomial.coeff_mul_C _ _ _

@[simp]
lemma coeff_natCast_mul {R : Type*} [Semiring R] {p : R[X]} {a : ℕ} : coeff ((a : R[X]) * p) k = a * coeff p k := Polynomial.coeff_C_mul _

@[simp]
lemma coeff_mul_intCast {R : Type*} [Ring R] {p : R[X]} {a : ℤ} : coeff (p * (a : R[X])) k = coeff p k * (↑a : R) := Polynomial.coeff_mul_C _ _ _

@[simp]
lemma coeff_intCast_mul {R : Type*} [Ring R] {p : R[X]} {a : ℤ} : coeff ((a : R[X]) * p) k = a * coeff p k := Polynomial.coeff_C_mul _

which should fix the confluence issue

[Gareth Ma]

Looks great!

[Gareth Ma]

These will be especially useful since it seems that some university courses uses polynomials as their primary introduction example

[Gareth Ma]

So an easy API gives a good impression

[Eric Wieser]

@Alex J. Best, can you add the ofNat versions too?