R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
this : Decidable (∃ x, IsRoot p x)
h✝ : ∃ x, IsRoot p x
x : R
hp : 0 ≠ 0
hx : IsRoot p x
hpd : 0 < degree p
h : p /ₘ (X - ↑C x) = 0
⊢ False
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h✝ : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
h : p /ₘ (X - ↑C x) = 0
⊢ False
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, MulZeroClass.mul_zero] at hp
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
this : Decidable (∃ x, IsRoot p x)
h✝ : ∃ x, IsRoot p x
x : R
hp : 0 ≠ 0
hx : IsRoot p x
hpd : 0 < degree p
h : p /ₘ (X - ↑C x) = 0
⊢ False
exact hp rfl
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
⊢ 0 < 1
decide
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
⊢ 1 ≤ ↑(natDegree p)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
⊢ degree (X - ↑C x) ≤ degree p
rw [degree_X_sub_C, degree_eq_natDegree hp]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < ↑(natDegree p)
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
⊢ 1 ≤ ↑(natDegree p)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
⊢ 1 ≤ ↑(natDegree p)
rw [degree_eq_natDegree hp] at hpd
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < ↑(natDegree p)
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
⊢ 1 ≤ ↑(natDegree p)
exact WithBot.coe_le_coe.2 (WithBot.coe_lt_coe.1 hpd)
case e_a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ↑Multiset.card (x ::ₘ t) = Add.add (↑(↑Multiset.card t)) 1
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ↑(↑Multiset.card (x ::ₘ t)) = ↑(↑Multiset.card t) + 1
congr
no goals
case e_a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ↑Multiset.card (x ::ₘ t) = Add.add (↑(↑Multiset.card t)) 1
exact_mod_cast Multiset.card_cons _ _
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ 1 + ↑(↑Multiset.card t) ≤ 1 + degree (p /ₘ (X - ↑C x))
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ↑(↑Multiset.card t) + 1 ≤ degree p
rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ 1 + ↑(↑Multiset.card t) ≤ 1 + degree (p /ₘ (X - ↑C x))
exact add_le_add (le_refl (1 : WithBot ℕ)) htd
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p
change ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
⊢ ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p
intro a
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - ↑C x) * (p /ₘ (X - ↑C x)))
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p
conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - ↑C x) * (p /ₘ (X - ↑C x)))
rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
  rootMultiplicity_X_sub_C, ← htr a]
case inl
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t

case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
split_ifs with ha
no goals
case inl
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t
rw [ha, count_cons_self, add_comm]
no goals
case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ∃ x, IsRoot p x
x : R
hx : IsRoot p x
hpd : 0 < degree p
hd0 : p /ₘ (X - ↑C x) ≠ 0
wf : degree (p /ₘ (X - ↑C x)) < degree p
t : Multiset R
htd : ↑(↑Multiset.card t) ≤ degree (p /ₘ (X - ↑C x))
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - ↑C x))
hdeg : degree (X - ↑C x) ≤ degree p
hdiv0 : p /ₘ (X - ↑C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t
rw [count_cons_of_ne ha, zero_add]
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ¬∃ x, IsRoot p x
a : R
⊢ count a 0 = rootMultiplicity a p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ¬∃ x, IsRoot p x
⊢ ∀ (a : R), count a 0 = rootMultiplicity a p
intro a
no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, IsRoot p x)
h : ¬∃ x, IsRoot p x
a : R
⊢ count a 0 = rootMultiplicity a p
rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]