no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : p = 0
⊢ (X - ↑C a) ^ rootMultiplicity a p ∣ p
simp [h]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : ¬p = 0
⊢ (X - ↑C a) ^ Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) ∣ p
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : ¬p = 0
⊢ (X - ↑C a) ^ rootMultiplicity a p ∣ p
rw [rootMultiplicity_eq_multiplicity, dif_neg h]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
a : R
h : ¬p = 0
⊢ (X - ↑C a) ^ Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) ∣ p
exact multiplicity.pow_multiplicity_dvd _