case a
σ : Type u_3
τ : Type ?u.756968
R : Type u_1
S : Type u_2
T : Type ?u.756977
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
x✝ : R
⊢ ↑(RingHom.comp (map f) C) x✝ = ↑(RingHom.comp C f) x✝
σ : Type u_3
τ : Type ?u.756968
R : Type u_1
S : Type u_2
T : Type ?u.756977
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
⊢ RingHom.comp (map f) C = RingHom.comp C f
ext1
no goals
case a
σ : Type u_3
τ : Type ?u.756968
R : Type u_1
S : Type u_2
T : Type ?u.756977
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
x✝ : R
⊢ ↑(RingHom.comp (map f) C) x✝ = ↑(RingHom.comp C f) x✝
apply map_C