no goals
α : Type u_1
M : Type u_3
N : Type ?u.286502
P : Type ?u.286505
R : Type u_2
S : Type ?u.286511
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.286603
M' : Type ?u.286606
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
l : α →₀ R
s : Finset α
hs : l ∈ supported R R ↑s
x : α
x✝ : x ∈ s
hxg : ¬x ∈ l.support
⊢ ↑l x • v x = 0
rw [not_mem_support_iff.1 hxg, zero_smul]