R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree p ∈ support (p * ↑C a)
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree (p * ↑C a) = natDegree p
refine' eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) _
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ coeff (p * ↑C a) (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 : leadingCoeff p * a ≠ 0
⊢ natDegree p ∈ support (p * ↑C a)
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 : leadingCoeff p * a ≠ 0
⊢ coeff (p * ↑C a) (natDegree p) ≠ 0
rwa [coeff_mul_C]