R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find (_ : multiplicity.Finite (X - ↑C a) p)) =
    Nat.find (_ : multiplicity.Finite (X - ↑C a) 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]
p0 : p ≠ 0
a : R
⊢ rootMultiplicity a p = Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
dsimp [rootMultiplicity]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p✝ q p : R[X]
p0 : p ≠ 0
a : R
⊢ Nat.find (_ : multiplicity.Finite (X - ↑C a) p) = Nat.find (_ : multiplicity.Finite (X - ↑C a) 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]
p0 : p ≠ 0
a : R
⊢ (if h0 : p = 0 then 0 else Nat.find (_ : multiplicity.Finite (X - ↑C a) p)) =
    Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
rw [dif_neg p0]
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]
p0 : p ≠ 0
a : R
⊢ Nat.find (_ : multiplicity.Finite (X - ↑C a) p) = Nat.find (_ : multiplicity.Finite (X - ↑C a) p)
convert rfl