no goals
α : Type u_1
M : Type ?u.23059
N : Type u_2
P : Type ?u.23065
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (-f) g = neLocus f (-g)
rw [← neLocus_neg_neg, neg_neg]