R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ q * p /ₘ q = p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
⊢ q * p /ₘ q = p
nontriviality R
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ degree 0 < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ q * p /ₘ q = p
refine' (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], _⟩).1
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ ⊥ < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ degree 0 < degree q
rw [degree_zero]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ ⊥ < degree q
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hmo : Monic q
✝ : Nontrivial R
⊢ 0 + q * p = q * p
rw [zero_add]