R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : ↑(aeval r) (↑(expand R p) f) = ↑(aeval (r ^ p)) f
hg : ↑(aeval r) (↑(expand R p) g) = ↑(aeval (r ^ p)) g
⊢ ↑(aeval r) (↑(expand R p) (f + g)) = ↑(aeval (r ^ p)) (f + g)
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ ↑(aeval r) (↑(expand R p) P) = ↑(aeval (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 : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : ↑(aeval r) (↑(expand R p) f) = ↑(aeval (r ^ p)) f
hg : ↑(aeval r) (↑(expand R p) g) = ↑(aeval (r ^ p)) g
⊢ ↑(aeval r) (↑(expand R p) (f + g)) = ↑(aeval (r ^ p)) (f + g)
rw [AlgHom.map_add, aeval_add, aeval_add, hf, hg]
no goals
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ ↑(aeval r) (↑(expand R p) (↑C a)) = ↑(aeval (r ^ p)) (↑C a)
simp
no goals
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : ↑(aeval r) (↑(expand R p) (↑C a * X ^ n)) = ↑(aeval (r ^ p)) (↑C a * X ^ n)
⊢ ↑(aeval r) (↑(expand R p) (↑C a * X ^ (n + 1))) = ↑(aeval (r ^ p)) (↑C a * X ^ (n + 1))
simp