α : Type u_3
M : Type u_1
R : Type u_2
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type ?u.737176
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i : α, ↑Finsupp.equivFunOnFinite x_1 i • v i = x
α : Type u_3
M : Type u_1
R : Type u_2
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type ?u.737176
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, ∑ i : α, c i • v i = x
rw [Finsupp.equivFunOnFinite.surjective.exists]
α : Type u_3
M : Type u_1
R : Type u_2
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type ?u.737176
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : M
⊢ (∃ c, (Finsupp.sum c fun i a => a • v i) = x) ↔ ∃ x_1, ∑ x : α, ↑x_1 x • v x = x
α : Type u_3
M : Type u_1
R : Type u_2
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type ?u.737176
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i : α, ↑Finsupp.equivFunOnFinite x_1 i • v i = x
simp [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]
no goals
α : Type u_3
M : Type u_1
R : Type u_2
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type ?u.737176
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : M
⊢ (∃ c, (Finsupp.sum c fun i a => a • v i) = x) ↔ ∃ x_1, ∑ x : α, ↑x_1 x • v x = x
exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _