∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {v : α → M} {x : M}, x ∈ Submodule.span R (Set.range v) ↔ ∃ c, ∑ i, c i • v i = x