R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree p ∈ support (↑C a * p)
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree (↑C a * p) = natDegree p
refine' eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) _
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ coeff (↑C a * p) (natDegree p) ≠ 0
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree p ∈ support (↑C a * p)
refine' mem_support_iff.mpr _
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ coeff (↑C a * p) (natDegree p) ≠ 0
rwa [coeff_C_mul]