σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(rename g) (eval₂ C (X ∘ f) p) = ↑(rename (g ∘ f)) p
simp only [rename, aeval_eq_eval₂Hom]
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C = algebraMap R (MvPolynomial α R)
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) (fun x => X (g (f x))) p =
    eval₂ (algebraMap R (MvPolynomial α R)) (fun x => X (g (f x))) p
refine' eval₂Hom_congr _ rfl rfl
case a
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) x✝ =
    ↑(algebraMap R (MvPolynomial α R)) x✝
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C = algebraMap R (MvPolynomial α R)
ext1
no goals
case a
σ : Type u_1
τ : Type u_4
α : Type u_3
R : Type u_2
S : Type ?u.149749
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) x✝ =
    ↑(algebraMap R (MvPolynomial α R)) x✝
simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]