R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = ↑(eval₂Hom f g) (eval₂ C q p)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)
show _ = eval₂Hom f g (eval₂ C q p)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ (RingHom.comp (eval₂Hom f g) C) (↑(eval₂Hom f g) ∘ q) p
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = ↑(eval₂Hom f g) (eval₂ C q p)
rw [eval₂_comp_left (eval₂Hom f g)]
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ ↑f a = ↑(RingHom.comp (eval₂Hom f g) C) a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ (RingHom.comp (eval₂Hom f g) C) (↑(eval₂Hom f g) ∘ q) p
congr with a
no goals
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ ↑f a = ↑(RingHom.comp (eval₂Hom f g) C) a
simp