case _hq
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ Monic (X - ↑C a)
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ (X - ↑C a) * (f /ₘ (X - ↑C a)) = f - f %ₘ (X - ↑C a)
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
no goals
case _hq
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ Monic (X - ↑C a)
exact monic_X_sub_C a