## Stream: PR reviews

### Topic: polynomial.eval2_smul

#### Bolton Bailey (Feb 01 2021 at 04:40):

Looking at the code for polynomial.eval2_smul

@[simp] lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} :
eval₂ g x (s • p) = g s • eval₂ g x p :=
begin
simp only [eval₂, sum_smul_index, forall_const, zero_mul, g.map_zero, g.map_mul, mul_assoc],
-- Why doesn't rw [←finsupp.mul_sum] work?
convert (@finsupp.mul_sum _ _ _ _ _ (g s) p (λ i a, (g a * x ^ i))).symm,
end


Shouldn't the lemma be

@[simp] lemma eval₂_smul (g : R →+* S) (p : polynomial R) (x : S) {s : R} :
eval₂ g x (s • p) = g s * eval₂ g x p :=
...


As both g s and eval₂ g x p are in S

#### Bolton Bailey (Feb 01 2021 at 04:51):

Similar thing with polynomial.eval_smul

#### Johan Commelin (Feb 01 2021 at 05:49):

@Bolton Bailey (Aside: is this part of an existing PR? If so, you can write #1234 in the title of the thread, and it will create a link to PR 1234.)

I think the reason for using \bu in both places is for some sort of "regularity" in the operations on both sides. But maybe in practice using * on the RHS would be better. I don't have a strong opinion.

#### Bolton Bailey (Feb 01 2021 at 05:57):

It's not part of an existing PR, I was going to test the air here before writing one.
After wondering for a few days why the Infoview in my project was showing a coercion operation when I didn't think there should be one it seems like this is the reason. With that in mind, I think that the * is more natural, but I'll try to figure out if changing it fixes the issue.

#### Johan Commelin (Feb 01 2021 at 06:03):

Aha, but then you should probably use a different stream. (Not too big of an issue.) We try to use this stream only for discussion about explicit PRs. (See the other thread titles, they all have the format #1234 pr name.

#### Johan Commelin (Feb 01 2021 at 06:03):

But where is the coercion? Because there shouldn't be a coercion either.

#### Bolton Bailey (Feb 01 2021 at 08:42):

Thanks, in the future I'll open a PR before posting, and I'll make a PR for this as soon as I have time.

Here's a MWE of my case, where I am trying to reason about a polynomial that has been converted to a mv_polynomial using eval_2.

import data.polynomial.basic
import data.mv_polynomial.basic

section

universe u

parameter {S : Type}
parameter {F : Type u}
parameter [field F]

lemma foo (s : S) (i : F) (p : polynomial F) : polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) (i • p) = i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) (p) :=
begin
rw polynomial.eval₂_smul,
-- ⇑mv_polynomial.C i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) p =
-- i • polynomial.eval₂ mv_polynomial.C (mv_polynomial.X s) p
end

end


#### Eric Wieser (Feb 01 2021 at 08:44):

Where's the coercion?

#### Johan Commelin (Feb 01 2021 at 08:44):

Well, we enjoy discussions before PRs as well (-; But we put them in #general or #maths . (But no worries... it's not a big deal. I was just confused about whether I missed a PR that you were talking about.)

#### Eric Wieser (Feb 01 2021 at 08:45):

Are you talking about the function coercion right at the start? That's just how bundled functions work, and nothing to do with this lemma

#### Bolton Bailey (Feb 01 2021 at 09:03):
If that's how bundled functions look that's fine, but it's a bit surprising since nowhere in the code I write myself do I have to put ⇑ before mv_polynomial.C when calling it as a function.
It still seems to me that it should be * in the lemma - the \smul is on the left hand side because it has to be, but an smul on the right hand side is not what I expected. You can see the original author was confused as to why they couldn't use rw [←finsupp.mul_sum] - this indeed closes the lemma in the * version.