R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B] <;>
  simp [mul_sum, mul_assoc]