case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ↑ϕ p = eval₂ (RingHom.comp ϕ C) (fun s => ↑ϕ (X s)) p
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
⊢ ↑ϕ p = eval₂ (RingHom.comp ϕ C) (fun s => ↑ϕ (X s)) p
cases nonempty_fintype σ
case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ↑ϕ (∑ v in support p, ↑(monomial v) (coeff v p)) = eval₂ (RingHom.comp ϕ C) (fun s => ↑ϕ (X s)) p
case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ↑ϕ p = eval₂ (RingHom.comp ϕ C) (fun s => ↑ϕ (X s)) p
refine' Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) _
case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x in support p, ↑ϕ (↑(monomial x) (coeff x p)) =
    ∑ d in support p, ↑(RingHom.comp ϕ C) (coeff d p) * ∏ i : σ, ↑ϕ (X i) ^ ↑d i
case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ↑ϕ (∑ v in support p, ↑(monomial v) (coeff v p)) = eval₂ (RingHom.comp ϕ C) (fun s => ↑ϕ (X s)) p
rw [MvPolynomial.eval₂_eq', ϕ.map_sum]
case intro.e_f
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ (fun x => ↑ϕ (↑(monomial x) (coeff x p))) = fun d => ↑(RingHom.comp ϕ C) (coeff d p) * ∏ i : σ, ↑ϕ (X i) ^ ↑d i
case intro
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x in support p, ↑ϕ (↑(monomial x) (coeff x p)) =
    ∑ d in support p, ↑(RingHom.comp ϕ C) (coeff d p) * ∏ i : σ, ↑ϕ (X i) ^ ↑d i
congr
case intro.e_f.h
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
x✝ : σ →₀ ℕ
⊢ ↑ϕ (↑(monomial x✝) (coeff x✝ p)) = ↑(RingHom.comp ϕ C) (coeff x✝ p) * ∏ i : σ, ↑ϕ (X i) ^ ↑x✝ i
case intro.e_f
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ (fun x => ↑ϕ (↑(monomial x) (coeff x p))) = fun d => ↑(RingHom.comp ϕ C) (coeff d p) * ∏ i : σ, ↑ϕ (X i) ^ ↑d i
ext
no goals
case intro.e_f.h
R : Type u
S✝ : Type ?u.883146
σ : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S✝
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
x✝ : σ →₀ ℕ
⊢ ↑ϕ (↑(monomial x✝) (coeff x✝ p)) = ↑(RingHom.comp ϕ C) (coeff x✝ p) * ∏ i : σ, ↑ϕ (X i) ^ ↑x✝ i
simp only [monomial_eq, ϕ.map_pow, ϕ.map_prod, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]