no goals
σ : Type u_3
τ : Type u_4
α : Type ?u.73427
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
apply MvPolynomial.induction_on p
  (fun a => by simp only [map_C, rename_C])
  (fun p q hp hq => by simp only [hp, hq, AlgHom.map_add, RingHom.map_add]) fun p n hp => by
  simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]
no goals
σ : Type u_3
τ : Type u_4
α : Type ?u.73427
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ ↑(map f) (↑(rename g) (↑C a)) = ↑(rename g) (↑(map f) (↑C a))
simp only [map_C, rename_C]
no goals
σ : Type u_3
τ : Type u_4
α : Type ?u.73427
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p q : MvPolynomial σ R
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
hq : ↑(map f) (↑(rename g) q) = ↑(rename g) (↑(map f) q)
⊢ ↑(map f) (↑(rename g) (p + q)) = ↑(rename g) (↑(map f) (p + q))
simp only [hp, hq, AlgHom.map_add, RingHom.map_add]
no goals
σ : Type u_3
τ : Type u_4
α : Type ?u.73427
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
⊢ ↑(map f) (↑(rename g) (p * X n)) = ↑(rename g) (↑(map f) (p * X n))
simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]