polynomial.eval2_smul

Stream: PR reviews

[Bolton Bailey]

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]

Similar thing with polynomial.eval_smul

[Johan Commelin]

@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]

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]

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]

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

[Bolton Bailey]

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]

Where's the coercion?

[Johan Commelin]

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]

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]

Presumably a zulip admin can move this thread

[Bolton Bailey]

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.