no goals
σ : Type u_2
τ : Type u_3
α : Type ?u.892507
R : Type u_1
S : Type ?u.892513
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
⊢ eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
apply MvPolynomial.induction_on p (fun n => by simp only [eval₂_C, rename_C])
  (fun p q hp hq => by simp only [hp, hq, rename, eval₂_add, AlgHom.map_add])
  fun p n hp => by simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]
no goals
σ : Type u_2
τ : Type u_3
α : Type ?u.892507
R : Type u_1
S : Type ?u.892513
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
n : ℤ
⊢ eval₂ c (g ∘ f) (↑C n) = eval₂ c g (↑(rename f) (↑C n))
simp only [eval₂_C, rename_C]
no goals
σ : Type u_2
τ : Type u_3
α : Type ?u.892507
R : Type u_1
S : Type ?u.892513
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p q : MvPolynomial σ ℤ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
hq : eval₂ c (g ∘ f) q = eval₂ c g (↑(rename f) q)
⊢ eval₂ c (g ∘ f) (p + q) = eval₂ c g (↑(rename f) (p + q))
simp only [hp, hq, rename, eval₂_add, AlgHom.map_add]
no goals
σ : Type u_2
τ : Type u_3
α : Type ?u.892507
R : Type u_1
S : Type ?u.892513
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p : MvPolynomial σ ℤ
n : σ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
⊢ eval₂ c (g ∘ f) (p * X n) = eval₂ c g (↑(rename f) (p * X n))
simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]