no goals
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
⊢ eval₂ c (↑f ∘ X) x = ↑f x
apply MvPolynomial.induction_on x
  (fun n => by
    rw [hom_C f, eval₂_C]
    exact eq_intCast c n)
  (fun p q hp hq => by
    rw [eval₂_add, hp, hq]
    exact (f.map_add _ _).symm)
  (fun p n hp => by
    rw [eval₂_mul, eval₂_X, hp]
    exact (f.map_mul _ _).symm)
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ ↑c n = ↑n
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (↑f ∘ X) (↑C n) = ↑f (↑C n)
rw [hom_C f, eval₂_C]
no goals
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ ↑c n = ↑n
exact eq_intCast c n
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q✝ : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (↑f ∘ X) p = ↑f p
hq : eval₂ c (↑f ∘ X) q = ↑f q
⊢ ↑f p + ↑f q = ↑f (p + q)
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q✝ : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (↑f ∘ X) p = ↑f p
hq : eval₂ c (↑f ∘ X) q = ↑f q
⊢ eval₂ c (↑f ∘ X) (p + q) = ↑f (p + q)
rw [eval₂_add, hp, hq]
no goals
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q✝ : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (↑f ∘ X) p = ↑f p
hq : eval₂ c (↑f ∘ X) q = ↑f q
⊢ ↑f p + ↑f q = ↑f (p + q)
exact (f.map_add _ _).symm
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (↑f ∘ X) p = ↑f p
⊢ ↑f p * (↑f ∘ X) n = ↑f (p * X n)
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (↑f ∘ X) p = ↑f p
⊢ eval₂ c (↑f ∘ X) (p * X n) = ↑f (p * X n)
rw [eval₂_mul, eval₂_X, hp]
no goals
R✝ : Type u
S : Type v
σ : Type ?u.162485
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (↑f ∘ X) p = ↑f p
⊢ ↑f p * (↑f ∘ X) n = ↑f (p * X n)
exact (f.map_mul _ _).symm