case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X ^ Nat.zero) = eval x p * x ^ Nat.zero

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k : ℕ
ih : eval x (p * X ^ k) = eval x p * x ^ k
⊢ eval x (p * X ^ Nat.succ k) = eval x p * x ^ Nat.succ k
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k : ℕ
⊢ eval x (p * X ^ k) = eval x p * x ^ k
induction' k with k ih
no goals
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X ^ Nat.zero) = eval x p * x ^ Nat.zero
simp
no goals
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k : ℕ
ih : eval x (p * X ^ k) = eval x p * x ^ k
⊢ eval x (p * X ^ Nat.succ k) = eval x p * x ^ Nat.succ k
simp [pow_succ', ← mul_assoc, ih]