case zero
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ p : R[X]
⊢ (↑derivative^[Nat.zero]) (s • p) = s • (↑derivative^[Nat.zero]) p

case succ
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ : R[X]
k : ℕ
ih : ∀ (p : R[X]), (↑derivative^[k]) (s • p) = s • (↑derivative^[k]) p
p : R[X]
⊢ (↑derivative^[Nat.succ k]) (s • p) = s • (↑derivative^[Nat.succ k]) p
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (↑derivative^[k]) (s • p) = s • (↑derivative^[k]) p
induction' k with k ih generalizing p
no goals
case zero
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ p : R[X]
⊢ (↑derivative^[Nat.zero]) (s • p) = s • (↑derivative^[Nat.zero]) p
simp
no goals
case succ
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ : R[X]
k : ℕ
ih : ∀ (p : R[X]), (↑derivative^[k]) (s • p) = s • (↑derivative^[k]) p
p : R[X]
⊢ (↑derivative^[Nat.succ k]) (s • p) = s • (↑derivative^[Nat.succ k]) p
simp [ih]