no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R 1) (↑C r) = ↑C r
rw [expand_C]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f✝ f g : R[X]
ihf : ↑(expand R 1) f = f
ihg : ↑(expand R 1) g = g
⊢ ↑(expand R 1) (f + g) = f + g
rw [AlgHom.map_add, ihf, ihg]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : ↑(expand R 1) (↑C r * X ^ n) = ↑C r * X ^ n
⊢ ↑(expand R 1) (↑C r * X ^ (n + 1)) = ↑C r * X ^ (n + 1)
rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, pow_one]