case h
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = (comap f ∘ comap g) x
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (AlgHom.comp g f) = comap f ∘ comap g
funext x
no goals
case h
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = (comap f ∘ comap g) x
exact comap_comp_apply _ _ _