case hf
σ : Type u_4
τ : Type u_2
R : Type u_3
S : Type ?u.419424
T : Type ?u.419427
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ↑(AlgHom.comp (bind₁ g) (bind₁ f)) (X i✝) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) (X i✝)
σ : Type u_4
τ : Type u_2
R : Type u_3
S : Type ?u.419424
T : Type ?u.419427
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
⊢ AlgHom.comp (bind₁ g) (bind₁ f) = bind₁ fun i => ↑(bind₁ g) (f i)
ext1
no goals
case hf
σ : Type u_4
τ : Type u_2
R : Type u_3
S : Type ?u.419424
T : Type ?u.419427
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ↑(AlgHom.comp (bind₁ g) (bind₁ f)) (X i✝) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) (X i✝)
apply bind₁_bind₁