Theorems · Theorem · linear algebra

LinearIndependent.finite_of_le_span_finite

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} (v : ι → M),
  LinearIndependent R v → ∀ (w : Set M) [Finite ↑w], Set.range v ⊆ ↑(Submodule.span R w) → Finite ι

If R satisfies the strong rank condition, then any linearly independent family v : ι → M contained in the span of some finite w : Set M, is itself finite.

Defined in

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Cited by

2 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleStrongRankConditionFinite