R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑derivative (↑C ↑n) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑derivative ↑n = 0
rw [← C_eq_int_cast n]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑derivative (↑C ↑n) = 0
exact derivative_C