R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
p✝ q : MvPolynomial σ R
inst✝² : Algebra R S₁
inst✝¹ : CommSemiring S₂
f : σ → S₁
B : Type u_1
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ ↑φ (↑(aeval g) p) = ↑(RingHom.comp φ (eval₂Hom (algebraMap R S₁) fun i => g i)) p
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
p✝ q : MvPolynomial σ R
inst✝² : Algebra R S₁
inst✝¹ : CommSemiring S₂
f : σ → S₁
B : Type u_1
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ ↑φ (↑(aeval g) p) = ↑(eval₂Hom (RingHom.comp φ (algebraMap R S₁)) fun i => ↑φ (g i)) p
rw [← comp_eval₂Hom]
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
p✝ q : MvPolynomial σ R
inst✝² : Algebra R S₁
inst✝¹ : CommSemiring S₂
f : σ → S₁
B : Type u_1
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ ↑φ (↑(aeval g) p) = ↑(RingHom.comp φ (eval₂Hom (algebraMap R S₁) fun i => g i)) p
rfl