R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
nontriviality
case inl
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : degree p < 0
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p

case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < degree p
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
cases' hp.lt_or_lt with hd hd
case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < degree p
⊢ degree (X - ↑C a) ≤ degree p
case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < degree p
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
refine' leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) _
no goals
case inr
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < degree p
⊢ degree (X - ↑C a) ≤ degree p
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]
no goals
case inl
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
p✝ q p : R[X]
hp : degree p ≠ 0
a : R
inst✝ : Nontrivial R
hd : degree p < 0
⊢ leadingCoeff (p /ₘ (X - ↑C a)) = leadingCoeff p
rw [degree_eq_bot.mp <| (Nat.WithBot.lt_zero_iff _).mp hd, zero_divByMonic]