case a
σ : Type u_3
τ : Type ?u.929356
R : Type u_1
S : Type u_2
T : Type ?u.929365
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
r : R
⊢ ↑(RingHom.comp (eval₂Hom f g) C) r = ↑f r
σ : Type u_3
τ : Type ?u.929356
R : Type u_1
S : Type u_2
T : Type ?u.929365
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
⊢ RingHom.comp (eval₂Hom f g) C = f
ext1 r
no goals
case a
σ : Type u_3
τ : Type ?u.929356
R : Type u_1
S : Type u_2
T : Type ?u.929365
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
r : R
⊢ ↑(RingHom.comp (eval₂Hom f g) C) r = ↑f r
exact eval₂_C f g r