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' : eval a (↑derivative f) ≠ 0
⊢ ¬X - ↑C a ∣ f /ₘ (X - ↑C 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' : eval a (↑derivative f) ≠ 0
⊢ IsCoprime (X - ↑C a) (f /ₘ (X - ↑C a))
refine Or.resolve_left
    (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
      (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C 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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
⊢ eval a (↑derivative f) = 0
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' : eval a (↑derivative f) ≠ 0
⊢ ¬X - ↑C a ∣ f /ₘ (X - ↑C a)
contrapose! hf' with h
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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
this : X - ↑C a ∣ ↑derivative f
⊢ eval a (↑derivative f) = 0
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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
⊢ eval a (↑derivative f) = 0
have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
this : ↑C (eval a (↑derivative f)) = 0
⊢ eval a (↑derivative f) = 0
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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
this : X - ↑C a ∣ ↑derivative f
⊢ eval a (↑derivative f) = 0
rw [← dvd_iff_modByMonic_eq_zero (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
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
h : X - ↑C a ∣ f /ₘ (X - ↑C a)
this : ↑C (eval a (↑derivative f)) = 0
⊢ eval a (↑derivative f) = 0
rwa [← C_inj, C_0]