no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R p) (↑(expand R q) (↑C r)) = ↑(expand R (p * q)) (↑C r)
simp_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 p) (↑(expand R q) f) = ↑(expand R (p * q)) f
ihg : ↑(expand R p) (↑(expand R q) g) = ↑(expand R (p * q)) g
⊢ ↑(expand R p) (↑(expand R q) (f + g)) = ↑(expand R (p * q)) (f + g)
simp_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 p) (↑(expand R q) (↑C r * X ^ n)) = ↑(expand R (p * q)) (↑C r * X ^ n)
⊢ ↑(expand R p) (↑(expand R q) (↑C r * X ^ (n + 1))) = ↑(expand R (p * q)) (↑C r * X ^ (n + 1))
simp_rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, AlgHom.map_pow, expand_X, pow_mul]