F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ ↑derivative f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ ↑derivative f
conv_lhs => rw [hg3, ← hu]
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ ↑derivative f
rwa [Units.mul_right_dvd]