R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
⊢ leadingCoeff (p /ₘ q) = leadingCoeff p
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
⊢ leadingCoeff (p /ₘ q) = leadingCoeff p
nontriviality
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ leadingCoeff (p /ₘ q) = leadingCoeff p
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
⊢ leadingCoeff (p /ₘ q) = leadingCoeff p
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
  simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
    Nat.WithBot.one_le_iff_zero_lt] using hdegree
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ leadingCoeff (p /ₘ q) = leadingCoeff (p %ₘ q + q * (p /ₘ q))
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ leadingCoeff (p /ₘ q) = leadingCoeff p
nth_rw 2 [← modByMonic_add_div p hmonic]
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree (p %ₘ q) < degree (q * (p /ₘ q))
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ leadingCoeff (p /ₘ q) = leadingCoeff (p %ₘ q + q * (p /ₘ q))
rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree (p %ₘ q) < degree p
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree (p %ₘ q) < degree (q * (p /ₘ q))
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]
no goals
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
h : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
⊢ degree (p %ₘ q) < degree p
exact (degree_modByMonic_lt p hmonic).trans_le hdegree
no goals
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : Monic q
hdegree : degree q ≤ degree p
✝ : Nontrivial R
⊢ leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
  Nat.WithBot.one_le_iff_zero_lt] using hdegree