case h
ι : Type u_1
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
inst✝ : Fintype ι
f : ι →₀ { x // x ∈ I }
⊢ ∀ (i : ι), ↑0 • v i = 0
ι : Type u_1
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
inst✝ : Fintype ι
f : ι →₀ { x // x ∈ I }
⊢ ↑(finsuppTotal ι M I v) f = ∑ i : ι, ↑(↑f i) • v i
rw [finsuppTotal_apply, Finsupp.sum_fintype]
no goals
case h
ι : Type u_1
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
inst✝ : Fintype ι
f : ι →₀ { x // x ∈ I }
⊢ ∀ (i : ι), ↑0 • v i = 0
exact fun _ => zero_smul _ _