no goals
α : Type u_3
M : Type u_1
N : Type ?u.375591
P : Type ?u.375594
R : Type u_2
S : Type ?u.375600
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.375692
M' : Type ?u.375695
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v✝ : α → M
v' : α' → M'
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, (sum c fun i a => a • v i) = x
simp only [← Finsupp.range_total, LinearMap.mem_range, Finsupp.total_apply]