R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ Finset.min (support (-p)) = Finset.min (support p)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ trailingDegree (-p) = trailingDegree p
unfold trailingDegree
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ Finset.min (support (-p)) = Finset.min (support p)
rw [support_neg]