no goals
M : Type u_2
inst✝⁴ : Monoid M
R : Type ?u.35641
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_1
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ eval (m • x) (m • ↑C r) = m • eval x (↑C r)
rw [smul_C, eval_C, eval_C]
no goals
M : Type u_2
inst✝⁴ : Monoid M
R : Type ?u.35641
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_1
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
no goals
M : Type u_2
inst✝⁴ : Monoid M
R : Type ?u.35641
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_1
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (↑C r * X ^ n)) = m • eval x (↑C r * X ^ n)
⊢ eval (m • x) (m • (↑C r * X ^ (n + 1))) = m • eval x (↑C r * X ^ (n + 1))
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C,
  eval_pow, eval_X, smul_mul', smul_pow']