R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r (↑(expand R p) f) = eval (r ^ p) f
hg : eval r (↑(expand R p) g) = eval (r ^ p) g
⊢ eval r (↑(expand R p) (f + g)) = eval (r ^ p) (f + g)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
⊢ eval r (↑(expand R p) P) = eval (r ^ p) P
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r (↑(expand R p) f) = eval (r ^ p) f
hg : eval r (↑(expand R p) g) = eval (r ^ p) g
⊢ eval r (↑(expand R p) (f + g)) = eval (r ^ p) (f + g)
rw [AlgHom.map_add, eval_add, eval_add, hf, hg]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r a : R
⊢ eval r (↑(expand R p) (↑C a)) = eval (r ^ p) (↑C a)
simp
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r (↑(expand R p) (↑C a * X ^ n)) = eval (r ^ p) (↑C a * X ^ n)
⊢ eval r (↑(expand R p) (↑C a * X ^ (n + 1))) = eval (r ^ p) (↑C a * X ^ (n + 1))
simp