R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 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 : R[X]
a : R
h0 : p ≠ 0
⊢ multiplicity.Finite (X - ↑C a) p
haveI := Nontrivial.of_polynomial_ne h0
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < degree (X - ↑C a)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ multiplicity.Finite (X - ↑C a) p
refine' multiplicity_finite_of_degree_pos_of_monic _ (monic_X_sub_C _) h0
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < degree (X - ↑C a)
rw [degree_X_sub_C]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
decide