R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
⊢ X - ↑C a ∣ ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
⊢ X - ↑C a ∣ ↑derivative f
have key := divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative f a
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
u : K[X]
hu : f /ₘ (X - ↑C a) = (X - ↑C a) * u
⊢ X - ↑C a ∣ ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
⊢ X - ↑C a ∣ ↑derivative f
have ⟨u,hu⟩ := hf
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
u : K[X]
hu : f /ₘ (X - ↑C a) = (X - ↑C a) * u
⊢ X - ↑C a ∣ (X - ↑C a) * (u + ↑derivative ((X - ↑C a) * u))
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
u : K[X]
hu : f /ₘ (X - ↑C a) = (X - ↑C a) * u
⊢ X - ↑C a ∣ ↑derivative f
rw [←key, hu, ←mul_add (X - C a) u _]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - ↑C a ∣ f /ₘ (X - ↑C a)
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
u : K[X]
hu : f /ₘ (X - ↑C a) = (X - ↑C a) * u
⊢ X - ↑C a ∣ (X - ↑C a) * (u + ↑derivative ((X - ↑C a) * u))
use (u + derivative ((X - C a) * u))