R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : DivisionRing R
p✝ q p : R[X]
h : q ≠ 0
h₁ : (leadingCoeff q)⁻¹ ≠ 0
⊢ degree (p * ↑C (leadingCoeff q)⁻¹) = degree p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : DivisionRing R
p✝ q p : R[X]
h : q ≠ 0
⊢ degree (p * ↑C (leadingCoeff q)⁻¹) = degree p
have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : DivisionRing R
p✝ q p : R[X]
h : q ≠ 0
h₁ : (leadingCoeff q)⁻¹ ≠ 0
⊢ degree (p * ↑C (leadingCoeff q)⁻¹) = degree p
rw [degree_mul, degree_C h₁, add_zero]