σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) p = ↑(map f) p
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑f (_ : ↑f 0 = 0) p = ↑(map f) p
change Finsupp.mapRange (f : R →+ S) (f : R →+ S).map_zero p = map f p
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x in support p, Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial x) (coeff x p)) =
    ∑ x in support p, ↑(map f) (↑(monomial x) (coeff x p))
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) p = ↑(map f) p
rw [p.as_sum, Finsupp.mapRange_finset_sum, (map f).map_sum]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial n) (coeff n p)) = ↑(map f) (↑(monomial n) (coeff n p))
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x in support p, Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial x) (coeff x p)) =
    ∑ x in support p, ↑(map f) (↑(monomial x) (coeff x p))
refine' Finset.sum_congr rfl fun n _ => _
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ ↑(monomial n) (↑↑f (coeff n p)) = ↑(monomial n) (↑f (coeff n p))
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial n) (coeff n p)) = ↑(map f) (↑(monomial n) (coeff n p))
rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
no goals
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ ↑(monomial n) (↑↑f (coeff n p)) = ↑(monomial n) (↑f (coeff n p))
simp_all only [AddMonoidHom.coe_coe]