case hf
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
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
i : σ
⊢ ↑(AlgHom.comp φ (aeval f)) (X i) = ↑(aeval fun i => ↑φ (f i)) (X i)
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
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
⊢ AlgHom.comp φ (aeval f) = aeval fun i => ↑φ (f i)
ext i
no goals
case hf
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
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
i : σ
⊢ ↑(AlgHom.comp φ (aeval f)) (X i) = ↑(aeval fun i => ↑φ (f i)) (X i)
simp