α : Type u_1
β : Type u_3
γ : Type ?u.158167
ι : Type ?u.158170
M : Type u_2
M' : Type ?u.158176
N : Type ?u.158179
P : Type ?u.158182
G : Type ?u.158185
H : Type ?u.158188
R : Type ?u.158191
S : Type ?u.158194
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
x : α →₀ M
a : β
h : ¬a ∈ Set.range f
⊢ ∑ a_1 in x.support, ↑(single (f a_1) (↑x a_1)) a = 0
α : Type u_1
β : Type u_3
γ : Type ?u.158167
ι : Type ?u.158170
M : Type u_2
M' : Type ?u.158176
N : Type ?u.158179
P : Type ?u.158182
G : Type ?u.158185
H : Type ?u.158188
R : Type ?u.158191
S : Type ?u.158194
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
x : α →₀ M
a : β
h : ¬a ∈ Set.range f
⊢ ↑(mapDomain f x) a = 0
rw [mapDomain, sum_apply, sum]
no goals
α : Type u_1
β : Type u_3
γ : Type ?u.158167
ι : Type ?u.158170
M : Type u_2
M' : Type ?u.158176
N : Type ?u.158179
P : Type ?u.158182
G : Type ?u.158185
H : Type ?u.158188
R : Type ?u.158191
S : Type ?u.158194
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
x : α →₀ M
a : β
h : ¬a ∈ Set.range f
⊢ ∑ a_1 in x.support, ↑(single (f a_1) (↑x a_1)) a = 0
exact Finset.sum_eq_zero fun a' _ => single_eq_of_ne fun eq => h <| eq ▸ Set.mem_range_self _