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
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - ↑C a) ^ rootMultiplicity a p) ≠ 0
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
hp : p ≠ 0
⊢ eval a (p /ₘ (X - ↑C a) ^ rootMultiplicity a p) ≠ 0
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
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
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - ↑C a ∣ p /ₘ (X - ↑C a) ^ rootMultiplicity 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]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - ↑C a) ^ rootMultiplicity a p) ≠ 0
rw [Ne.def, ← IsRoot.def, ← dvd_iff_isRoot]
case intro
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
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
⊢ False
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
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - ↑C a ∣ p /ₘ (X - ↑C a) ^ rootMultiplicity a p
rintro ⟨q, hq⟩
case intro
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
⊢ False
case intro
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
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
⊢ False
have := divByMonic_mul_pow_rootMultiplicity_eq p a
case intro
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ False
case intro
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
⊢ False
rw [mul_comm, hq, ← mul_assoc, ← pow_succ', rootMultiplicity_eq_multiplicity, dif_neg hp] at this
no goals
case intro
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ False
exact
  multiplicity.is_greatest'
    (multiplicity_finite_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; exact by decide)
      (monic_X_sub_C _) hp)
    (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < 1
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 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✝ p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < 1
exact by decide
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
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - ↑C a) ^ rootMultiplicity a p = (X - ↑C a) * q
this : (X - ↑C a) ^ (Part.get (multiplicity (X - ↑C a) p) (_ : multiplicity.Finite (X - ↑C a) p) + 1) * q = p
⊢ 0 < 1
decide