no goals
α : Type u_1
M : Type ?u.32849
N : Type u_2
P : Type ?u.32855
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f (f + g) = g.support
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]