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
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = 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
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
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
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p =
    0 + (X - ↑C a) ^ rootMultiplicity a p * (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
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p = p
conv_rhs =>
    rw [← modByMonic_add_div p this,
      (dvd_iff_modByMonic_eq_zero this).2 (pow_rootMultiplicity_dvd _ _)]
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
this : Monic ((X - ↑C a) ^ rootMultiplicity a p)
⊢ p /ₘ (X - ↑C a) ^ rootMultiplicity a p * (X - ↑C a) ^ rootMultiplicity a p =
    0 + (X - ↑C a) ^ rootMultiplicity a p * (p /ₘ (X - ↑C a) ^ rootMultiplicity a p)
simp [mul_comm]