English
Let α be a set and N a cancellative AddRightCancelMonoid. For any finsupp f,g,h : α →₀ N, the set of coordinates where f and g differ is unchanged after adding h to both: (f + h).neLocus (g + h) = f.neLocus g.
Русский
Пусть α — множество, N — моноид с правой отменой для сложения. Пусть f,g,h : α →₀ N. Тогда множество координат, на которых f и g различаются, сохраняется при добавлении одного и того же h к обеим функциям: (f + h).neLocus (g + h) = f.neLocus g.
LaTeX
$$$ (f + h).neLocus (g + h) = f.neLocus g $$$
Lean4
@[simp]
theorem neLocus_add_right [AddRightCancelMonoid N] (f g h : α →₀ N) : (f + h).neLocus (g + h) = f.neLocus g :=
zipWith_neLocus_eq_right _ _ _ _ add_left_injective
