R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ (m : ℕ), m < n → ¬¬(X - ↑C a) ^ (m + 1) ∣ p) ↔ (X - ↑C a) ^ n ∣ p
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - ↑C a) ^ n ∣ p
rw [rootMultiplicity_eq_nat_find_of_nonzero p0, Nat.le_find_iff]
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ (m : ℕ), m < n → (X - ↑C a) ^ (m + 1) ∣ p) ↔ (X - ↑C a) ^ n ∣ p
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ (m : ℕ), m < n → ¬¬(X - ↑C a) ^ (m + 1) ∣ p) ↔ (X - ↑C a) ^ n ∣ p
simp_rw [Classical.not_not]
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ (m : ℕ), m < n → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ n ∣ p
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ (m : ℕ), m < n → (X - ↑C a) ^ (m + 1) ∣ p) ↔ (X - ↑C a) ^ n ∣ p
refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
case zero
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ (m : ℕ), m < Nat.zero → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ Nat.zero ∣ p

case succ
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ (m : ℕ), m < Nat.succ n → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ Nat.succ n ∣ p
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ (m : ℕ), m < n → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ n ∣ p
cases' n with n
case zero
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ (m : ℕ), m < Nat.zero → (X - ↑C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p
case zero
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ (m : ℕ), m < Nat.zero → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ Nat.zero ∣ p
rw [pow_zero]
no goals
case zero
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ (m : ℕ), m < Nat.zero → (X - ↑C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p
apply one_dvd
no goals
case succ
R : Type u
S : Type v
T : Type w
a✝ b : R
n✝ : ℕ
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ (m : ℕ), m < Nat.succ n → (X - ↑C a) ^ (m + 1) ∣ p
⊢ (X - ↑C a) ^ Nat.succ n ∣ p
exact h n n.lt_succ_self