no goals
R : Type u
S : Type v
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q a b : MvPolynomial σ R
⊢ totalDegree (a - b) = totalDegree (a + -b)
rw [sub_eq_add_neg]
no goals
R : Type u
S : Type v
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q a b : MvPolynomial σ R
⊢ max (totalDegree a) (totalDegree (-b)) = max (totalDegree a) (totalDegree b)
rw [totalDegree_neg]