R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : p %ₘ q = 0
⊢ q ∣ p
rw [← modByMonic_add_div p hq, h, zero_add]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
exact dvd_mul_right _ _
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
⊢ p %ₘ q = 0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
⊢ p %ₘ q = 0
nontriviality R
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
⊢ p %ₘ q = 0
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0
by_contra hpq0
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ False
have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ False
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
⊢ False
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
  hpq0 <|
    leadingCoeff_eq_zero.1
      (by rw [hmod, leadingCoeff_eq_zero.1 h, MulZeroClass.mul_zero, leadingCoeff_zero])
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑(natDegree q) + ↑(natDegree (r - p /ₘ q)) < ↑(natDegree q)
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
case intro
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] 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 : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑(natDegree q) + ↑(natDegree (r - p /ₘ q)) < ↑(natDegree q)
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
⊢ False
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.some_lt_some.1 this)
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)
rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h✝ : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
h : leadingCoeff (r - p /ₘ q) = 0
⊢ leadingCoeff (p %ₘ q) = 0
rw [hmod, leadingCoeff_eq_zero.1 h, MulZeroClass.mul_zero, leadingCoeff_zero]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
h : q ∣ p
✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : degree (q * (r - p /ₘ q)) < degree q
hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0
⊢ leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0
rwa [Monic.def.1 hq, one_mul]