R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ↑derivative (map f p) = map f (↑derivative p)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ ↑derivative (map f p) = map f (↑derivative p)
let n := max p.natDegree (map f p).natDegree
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ↑derivative (map f p) = map f (↑derivative p)
rw [derivative_apply, derivative_apply]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1))
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∑ a in range (n + 1), ↑C (coeff (map f p) a * ↑a) * X ^ (a - 1) =
    map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∑ a in range (n + 1), ↑C (coeff (map f p) a * ↑a) * X ^ (a - 1) =
    map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
  map_natCast, Polynomial.map_nat_cast, Polynomial.map_pow, map_X]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
all_goals intro n; rw [zero_mul, C_0, zero_mul]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max (natDegree p) (natDegree (map f p))
n : ℕ
⊢ ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
intro n
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max (natDegree p) (natDegree (map f p))
n : ℕ
⊢ ↑C (0 * ↑n) * X ^ (n - 1) = 0
rw [zero_mul, C_0, zero_mul]