# mathlibdocumentation

data.finsupp.ne_locus

# Locus of unequal values of finitely supported functions #

Let α N be two Types, assume that N has a 0 and let f g : α →₀ N be finitely supported functions.

## Main definition #

• finsupp.ne_locus f g : finset α, the finite subset of α where f and g differ.

In the case in which N is an additive group, finsupp.ne_locus f g coincides with finsupp.support (f - g).

def finsupp.ne_locus {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f g : α →₀ N) :

Given two finitely supported functions f g : α →₀ N, finsupp.ne_locus f g is the finset where f and g differ. This generalizes (f - g).support to situations without subtraction.

Equations
@[simp]
theorem finsupp.mem_ne_locus {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] {f g : α →₀ N} {a : α} :
a f.ne_locus g f a g a
@[simp]
theorem finsupp.coe_ne_locus {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f g : α →₀ N) :
(f.ne_locus g) = {x : α | f x g x}
@[simp]
theorem finsupp.ne_locus_eq_empty {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] {f g : α →₀ N} :
f.ne_locus g = f = g
@[simp]
theorem finsupp.nonempty_ne_locus_iff {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] {f g : α →₀ N} :
theorem finsupp.ne_locus_comm {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f g : α →₀ N) :
@[simp]
theorem finsupp.ne_locus_zero_right {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f : α →₀ N) :
@[simp]
theorem finsupp.ne_locus_zero_left {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] (f : α →₀ N) :
theorem finsupp.subset_map_range_ne_locus {α : Type u_1} {M : Type u_2} {N : Type u_3} [decidable_eq α] [decidable_eq N] [has_zero N] [decidable_eq M] [has_zero M] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0) :
F0 f).ne_locus F0 g) f.ne_locus g
theorem finsupp.zip_with_ne_locus_eq_left {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [decidable_eq α] [decidable_eq N] [has_zero M] [decidable_eq P] [has_zero P] [has_zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f : α →₀ M) (g₁ g₂ : α →₀ N) (hF : ∀ (f : M), function.injective (λ (g : N), F f g)) :
F0 f g₁).ne_locus F0 f g₂) = g₁.ne_locus g₂
theorem finsupp.zip_with_ne_locus_eq_right {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [decidable_eq α] [decidable_eq M] [has_zero M] [decidable_eq P] [has_zero P] [has_zero N] {F : M → N → P} (F0 : F 0 0 = 0) (f₁ f₂ : α →₀ M) (g : α →₀ N) (hF : ∀ (g : N), function.injective (λ (f : M), F f g)) :
F0 f₁ g).ne_locus F0 f₂ g) = f₁.ne_locus f₂
theorem finsupp.map_range_ne_locus_eq {α : Type u_1} {M : Type u_2} {N : Type u_3} [decidable_eq α] [decidable_eq N] [decidable_eq M] [has_zero M] [has_zero N] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0) (hF : function.injective F) :
F0 f).ne_locus F0 g) = f.ne_locus g
@[simp]
theorem finsupp.add_ne_locus_add_eq_left {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] (f g h : α →₀ N) :
(f + g).ne_locus (f + h) = g.ne_locus h
@[simp]
theorem finsupp.add_ne_locus_add_eq_right {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] (f g h : α →₀ N) :
(f + h).ne_locus (g + h) = f.ne_locus g
@[simp]
theorem finsupp.neg_ne_locus_neg {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [add_group N] (f g : α →₀ N) :
(-f).ne_locus (-g) = f.ne_locus g
theorem finsupp.ne_locus_neg {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [add_group N] (f g : α →₀ N) :
(-f).ne_locus g = f.ne_locus (-g)
theorem finsupp.ne_locus_eq_support_sub {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [add_group N] (f g : α →₀ N) :
f.ne_locus g = (f - g).support
@[simp]
theorem finsupp.sub_ne_locus_sub_eq_left {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [add_group N] (f g h : α →₀ N) :
(f - g).ne_locus (f - h) = g.ne_locus h
@[simp]
theorem finsupp.sub_ne_locus_sub_eq_right {α : Type u_1} {N : Type u_3} [decidable_eq α] [decidable_eq N] [add_group N] (f g h : α →₀ N) :
(f - h).ne_locus (g - h) = f.ne_locus g