replacement of `finset.sum_hom`

Stream: Is there code for X?

[Jon Eugster]

import data.polynomial

variables {A K: Type*} [comm_ring A] [is_domain A] [field K] [algebra A K]

example (p:polynomial A) (y:K) (d: K):
  d * (p.support.sum (λ (n : ℕ), (algebra_map A K) ((p.coeff n)) * y ^ n)) = (p.support.sum (λ (n : ℕ), d * (algebra_map A K) ((p.coeff n)) * y ^ n)) :=
begin
  sorry
end
-- Old proof: (polynomial.support p).sum_hom(has_mul.mul d)

I did some calculations with polynomials about a year ago and I used finset.sum_hom. Now I updated mathlib and it is gone, could you help me finding what the replacement would be? Is there a neat way to search old versions of mathlib or would I have to dig manually into the git-tree?

[Yaël Dillies]

Is it docs#add_monoid_hom.map_sum by any chance?

[Reid Barton]

Have you tried library_search?

[Jon Eugster]

Yaël Dillies said:

Is it docs#add_monoid_hom.map_sum by any chance?

Yes, I think that's almost it, thanks! Now I just have some problems actually using it, hmm...

[Yaël Dillies]

This lemma is soon getting refactoring as part of the hom refactor. Maybe your problem is related?

[Yaël Dillies]

You'll need to use docs#add_monoid_hom.mul_left btw

[Jon Eugster]

import algebra.big_operators
import data.polynomial

variables {A K: Type*} [comm_ring A] [is_domain A] [field K] [algebra A K]

example (p:polynomial A) (y:K) (d: ℚ):
  ↑d * (p.support.sum (λ (n : ℕ), y ^ n)) = (p.support.sum (λ (n : ℕ), ↑d * y ^ n)) :=
begin
  apply add_monoid_hom.map_sum (add_monoid_hom.mul_left (d:K)) (λ(n:ℕ), y ^ n) p.support,
end

Thank you Yaël, that worked!