σ : Type u_4
τ : Type u_3
R : Type u_1
S : Type u_2
T : Type ?u.836499
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom C fun i => ↑(map f) (g i)) (↑(map f) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
σ : Type u_4
τ : Type u_3
R : Type u_1
S : Type u_2
T : Type ?u.836499
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(bind₁ g) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]
no goals
σ : Type u_4
τ : Type u_3
R : Type u_1
S : Type u_2
T : Type ?u.836499
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom C fun i => ↑(map f) (g i)) (↑(map f) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
rfl