R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.708718
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type ?u.711370
M' : Type ?u.711373
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q)
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.708718
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type ?u.711370
M' : Type ?u.711373
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ ↑(comp p) (p' • q) = Polynomial.comp p' p • ↑(comp p) q
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
no goals
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.708718
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type ?u.711370
M' : Type ?u.711373
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q)
rfl