# Zulip Chat Archive

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

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

Presumably a zulip admin can move this thread

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

Last updated: May 06 2021 at 11:23 UTC