Linear combinations from independence and from Noetherianity

This file collects two complements to Mathlib's description of the span of a family by linear combinations: membership in the span of a linearly independent family is witnessed by a unique finitely supported combination, and in a Noetherian module every sequence has a term that is a linear combination of its predecessors.

Main statements

• LinearIndependent.mem_span_range_iff_existsUnique: membership in the span of a linearly independent family is equivalent to having unique finitely supported coordinates.
• TauCeti.exists_sum_smul_eq_of_isNoetherian: in a Noetherian module some term of a sequence is a linear combination of its predecessors.

theorem LinearIndependent.mem_span_range_iff_existsUnique {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (h : LinearIndependent R v) (x : M) : x ∈ Submodule.span R (Set.range v) ↔ ∃! a : ι →₀ R, (a.sum fun (i : ι) (r : R) => r • v i) = x

An element lies in the span of a linearly independent family exactly when it has a unique finitely supported expression in that family.

theorem TauCeti.exists_sum_smul_eq_of_isNoetherian (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (v : ℕ → M) : ∃ (n : ℕ) (c : Fin n → R), ∑ i : Fin n, c i • v ↑i = v n

In a Noetherian module some term of a sequence is a linear combination of its predecessors. The spans of the initial segments of v form an increasing chain of submodules, which must stabilize; at the first repetition v n already lies in the span of the earlier terms.