doc-next-gen

Mathlib.LinearAlgebra.LinearIndependent.Basic

Module docstring

{"# Linear independence

This file collects basic consequences of linear (in)dependence and includes specialized tests for specific families of vectors.

Main statements

We prove several specialized tests for linear independence of families of vectors and of sets of vectors.

  • linearIndependent_empty_type: a family indexed by an empty type is linearly independent;
  • linearIndependent_unique_iff: if ι is a singleton, then LinearIndependent K v is equivalent to v default ≠ 0;
  • linearIndependent_sum: type-specific test for linear independence of families of vector fields;
  • linearIndependent_singleton: linear independence tests for set operations.

In many cases we additionally provide dot-style operations (e.g., LinearIndependent.union) to make the linear independence tests usable as hv.insert ha etc.

TODO

Rework proofs to hold in semirings, by avoiding the path through ker (Finsupp.linearCombination R v) = ⊥.

Tags

linearly dependent, linear dependence, linearly independent, linear independence

","The following lemmas use the subtype defined by a set in M as the index set ι. ","### Properties which require Ring R "}

LinearIndependent.restrict_scalars theorem
[Semiring K] [SMulWithZero R K] [Module K M] [IsScalarTower R K M] (hinj : Injective fun r : R ↦ r • (1 : K)) (li : LinearIndependent K v) : LinearIndependent R v
Full source 
/-- A set of linearly independent vectors in a module `M` over a semiring `K` is also linearly
independent over a subring `R` of `K`.

See also `LinearIndependent.restrict_scalars'` for a version with more convenient typeclass
assumptions.

TODO : `LinearIndepOn` version. -/
theorem LinearIndependent.restrict_scalars [Semiring K] [SMulWithZero R K] [Module K M]
    [IsScalarTower R K M] (hinj : Injective fun r : R ↦ r • (1 : K))
    (li : LinearIndependent K v) : LinearIndependent R v := by
  intro x y hxy
  let f := fun r : R => r • (1 : K)
  have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_
  · ext i
    exact hinj congr($this i)
  simpa [Finsupp.linearCombination, f, Finsupp.sum_mapRange_index]
Linear Independence Preserved Under Restriction of Scalars
Informal description
Let $R$ be a subring of a semiring $K$, and let $M$ be a module over $K$ with a compatible scalar multiplication structure (i.e., $[IsScalarTower R K M]$). Suppose the map $r \mapsto r \cdot 1_K$ from $R$ to $K$ is injective. If a family of vectors $v$ in $M$ is linearly independent over $K$, then it is also linearly independent over $R$.
Submodule.range_ker_disjoint theorem
{f : M →ₗ[R] M'} (hv : LinearIndependent R (f ∘ v)) : Disjoint (span R (range v)) (LinearMap.ker f)
Full source 
/-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
    spans a submodule disjoint from the kernel of `f`.
TODO : `LinearIndepOn` version. -/
theorem Submodule.range_ker_disjoint {f : M →ₗ[R] M'}
    (hv : LinearIndependent R (f ∘ v)) :
    Disjoint (span R (range v)) (LinearMap.ker f) := by
  rw [LinearIndependent, Finsupp.linearCombination_linear_comp] at hv
  rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
Disjointness of Span and Kernel under Linear Independence of Composed Vectors
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $f : M \to M'$ be a linear map. If the composition $f \circ v$ is a linearly independent family of vectors in $M'$, then the span of the range of $v$ is disjoint from the kernel of $f$. In other words, $\text{span}_R(\text{range}(v)) \cap \ker(f) = \{\mathbf{0}\}$.
LinearIndependent.map_of_injective_injectiveₛ theorem
{R' M' : Type*} [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : Injective i) (hj : Injective j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (j ∘ v)
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map, `j : M →+ M'` is a monoid map,
such that they are both injective, and compatible with the scalar
multiplications on `M` and `M'`, then `j` sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map_injOn`.
TODO : `LinearIndepOn` version. -/
theorem LinearIndependent.map_of_injective_injectiveₛ {R' M' : Type*}
    [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v)
    (i : R' → R) (j : M →+ M') (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (j ∘ v) := by
  rw [linearIndependent_iff'ₛ] at hv ⊢
  intro S r₁ r₂ H s hs
  simp_rw [comp_apply, ← hc, ← map_sum] at H
  exact hi <| hv _ _ _ (hj H) s hs
Preservation of Linear Independence under Injective Ring and Module Maps
Informal description
Let $R$ and $R'$ be semirings, and let $M$ and $M'$ be additive commutative monoids equipped with module structures over $R$ and $R'$ respectively. Given a linearly independent family of vectors $v$ in $M$ over $R$, an injective map $i : R' \to R$ between the scalar rings, and an injective additive monoid homomorphism $j : M \to M'$ that is compatible with the scalar multiplications (i.e., $j(i(r) \cdot m) = r \cdot j(m)$ for all $r \in R'$ and $m \in M$), then the composed family $j \circ v$ is linearly independent in $M'$ over $R'$.
LinearIndependent.map_of_surjective_injectiveₛ theorem
{R' M' : Type*} [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v) (i : R → R') (j : M →+ M') (hi : Surjective i) (hj : Injective j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v)
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map,
and `j : M →+ M'` is an injective monoid map, such that the scalar multiplications
on `M` and `M'` are compatible, then `j` sends linearly independent families
of vectors to linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map_injOn`.
TODO : `LinearIndepOn` version. -/
theorem LinearIndependent.map_of_surjective_injectiveₛ {R' M' : Type*}
    [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v)
    (i : R → R') (j : M →+ M') (hi : Surjective i) (hj : Injective j)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v) := by
  obtain ⟨i', hi'⟩ := hi.hasRightInverse
  refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
  · apply_fun i at h
    rwa [hi', hi'] at h
  rw [hc (i' r) m, hi']
Preservation of Linear Independence under Surjective Ring and Injective Module Maps
Informal description
Let $R$ and $R'$ be semirings, and let $M$ and $M'$ be additive commutative monoids equipped with module structures over $R$ and $R'$ respectively. Given a linearly independent family of vectors $v : \iota \to M$ over $R$, a surjective ring homomorphism $i : R \to R'$, and an injective additive monoid homomorphism $j : M \to M'$ that satisfies the compatibility condition $j(r \cdot m) = i(r) \cdot j(m)$ for all $r \in R$ and $m \in M$, then the composed family $j \circ v : \iota \to M'$ is linearly independent over $R'$.
LinearIndependent.map_injOn theorem
(hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (Set.range v))) : LinearIndependent R (f ∘ v)
Full source 
/-- If a linear map is injective on the span of a family of linearly independent vectors, then
the family stays linearly independent after composing with the linear map.
See `LinearIndependent.map` for the version with `Set.InjOn` replaced by `Disjoint`
when working over a ring. -/
theorem LinearIndependent.map_injOn (hv : LinearIndependent R v) (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (Set.range v))) : LinearIndependent R (f ∘ v) :=
  (f.linearIndependent_iff_of_injOn hf_inj).mpr hv
Preservation of Linear Independence under Injective Linear Maps on Span
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a linearly independent family of vectors in $M$. Given a linear map $f : M \to M'$ that is injective on the span of the range of $v$, the composed family $f \circ v : \iota \to M'$ is also linearly independent over $R$.
LinearIndepOn.map_injOn theorem
(hv : LinearIndepOn R v s) (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (v '' s))) : LinearIndepOn R (f ∘ v) s
Full source 
theorem LinearIndepOn.map_injOn (hv : LinearIndepOn R v s) (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (v '' s))) : LinearIndepOn R (f ∘ v) s :=
  (f.linearIndepOn_iff_of_injOn hf_inj).mpr hv
Preservation of Linear Independence under Injective Linear Maps on Span of Subset
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors. For any subset $s \subseteq \iota$, if the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$ and $f : M \to M'$ is a linear map that is injective on the span of $\{v_i\}_{i \in s}$, then the family $\{f(v_i)\}_{i \in s}$ is also linearly independent over $R$.
LinearIndepOn.comp_of_image theorem
{s : Set ι'} {f : ι' → ι} (h : LinearIndepOn R v (f '' s)) (hf : InjOn f s) : LinearIndepOn R (v ∘ f) s
Full source 
theorem LinearIndepOn.comp_of_image {s : Set ι'} {f : ι' → ι} (h : LinearIndepOn R v (f '' s))
    (hf : InjOn f s) : LinearIndepOn R (v ∘ f) s :=
  LinearIndependent.comp h _ (Equiv.Set.imageOfInjOn _ _ hf).injective
Linear Independence Preserved Under Injective Restriction of Index Set
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. For any subset $s \subseteq \iota'$ and function $f : \iota' \to \iota$, if the vectors $\{v_i\}_{i \in f(s)}$ are linearly independent over $R$ and $f$ is injective on $s$, then the composition $\{v_{f(j)}\}_{j \in s}$ is also linearly independent over $R$.
LinearIndepOn.image_of_comp theorem
(f : ι → ι') (g : ι' → M) (hs : LinearIndepOn R (g ∘ f) s) : LinearIndepOn R g (f '' s)
Full source 
theorem LinearIndepOn.image_of_comp (f : ι → ι') (g : ι' → M) (hs : LinearIndepOn R (g ∘ f) s) :
    LinearIndepOn R g (f '' s) := by
  nontriviality R
  have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
  exact (linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs
Linear Independence of Image under Composition of Functions
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $g : \iota' \to M$ a family of vectors. For any subset $s \subseteq \iota$ and function $f : \iota \to \iota'$, if the composition $\{g(f(i))\}_{i \in s}$ is linearly independent over $R$, then the vectors $\{g(j)\}_{j \in f(s)}$ are also linearly independent over $R$.
LinearIndepOn.id_image theorem
(hs : LinearIndepOn R v s) : LinearIndepOn R id (v '' s)
Full source 
theorem LinearIndepOn.id_image (hs : LinearIndepOn R v s) : LinearIndepOn R id (v '' s) :=
  LinearIndepOn.image_of_comp v id hs
Linear Independence of Image under Identity Function
Informal description
For any subset $s \subseteq \iota$ and any family of vectors $v : \iota \to M$ that is linearly independent on $s$ over a ring $R$, the image family $\{v(i)\}_{i \in s}$ is linearly independent over $R$ when viewed as a family indexed by itself (via the identity function).
LinearIndepOn_iff_linearIndepOn_image_injOn theorem
[Nontrivial R] : LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ InjOn v s
Full source 
theorem LinearIndepOn_iff_linearIndepOn_image_injOn [Nontrivial R] :
    LinearIndepOnLinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ InjOn v s :=
  ⟨fun h ↦ ⟨h.id_image, h.injOn⟩, fun h ↦ (linearIndepOn_iff_image h.2).2 h.1⟩
Characterization of Linear Independence via Image and Injectivity
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, $\iota$ a type, $s \subseteq \iota$ a subset, and $v : \iota \to M$ a family of vectors. The family $\{v_i\}_{i \in s}$ is linearly independent over $R$ if and only if the following two conditions hold: 1. The family $\{x\}_{x \in v(s)}$ (indexed by itself via the identity function) is linearly independent over $R$. 2. The restriction of $v$ to $s$ is injective.
linearIndepOn_congr theorem
{w : ι → M} (h : EqOn v w s) : LinearIndepOn R v s ↔ LinearIndepOn R w s
Full source 
theorem linearIndepOn_congr {w : ι → M} (h : EqOn v w s) :
    LinearIndepOnLinearIndepOn R v s ↔ LinearIndepOn R w s := by
  rw [LinearIndepOn, LinearIndepOn]
  convert Iff.rfl using 2
  ext x
  exact h.symm x.2
Equality of Functions Preserves Linear Independence on a Subset
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v, w : \iota \to M$ two families of vectors. For any subset $s \subseteq \iota$, if $v$ and $w$ are equal on $s$ (i.e., $v(i) = w(i)$ for all $i \in s$), then the family $v$ is linearly independent on $s$ if and only if the family $w$ is linearly independent on $s$.
LinearIndepOn.congr theorem
{w : ι → M} (hli : LinearIndepOn R v s) (h : EqOn v w s) : LinearIndepOn R w s
Full source 
theorem LinearIndepOn.congr {w : ι → M} (hli : LinearIndepOn R v s) (h : EqOn v w s) :
    LinearIndepOn R w s :=
  (linearIndepOn_congr h).1 hli
Preservation of Linear Independence under Function Equality on a Subset
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v, w : \iota \to M$ two families of vectors. For any subset $s \subseteq \iota$, if $v$ is linearly independent on $s$ and $v$ equals $w$ on $s$, then $w$ is also linearly independent on $s$.
LinearIndependent.group_smul theorem
{G : Type*} [hG : Group G] [MulAction G R] [SMul G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : ι → M} (hv : LinearIndependent R v) (w : ι → G) : LinearIndependent R (w • v)
Full source 
theorem LinearIndependent.group_smul {G : Type*} [hG : Group G] [MulAction G R]
    [SMul G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : ι → M}
    (hv : LinearIndependent R v) (w : ι → G) : LinearIndependent R (w • v) := by
  rw [linearIndependent_iff''ₛ] at hv ⊢
  intro s g₁ g₂ hgs hsum i
  refine (Group.isUnit (w i)).smul_left_cancel.mp ?_
  refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
  · simp_rw [hgs i hi]
  · simpa only [smul_assoc, smul_comm] using hsum
Group Action Preserves Linear Independence of Scaled Vectors
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $G$ a group acting on both $R$ and $M$ such that the actions are compatible via the scalar multiplication (i.e., $G$ acts as a tower of scalars and the actions commute). Given a linearly independent family of vectors $v : \iota \to M$ over $R$ and a family of group elements $w : \iota \to G$, the scaled family $w \cdot v$ (where $(w \cdot v)(i) = w(i) \cdot v(i)$) is also linearly independent over $R$.
LinearIndependent.group_smul_iff theorem
{G : Type*} [hG : Group G] [MulAction G R] [MulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : ι → M) (w : ι → G) : LinearIndependent R (w • v) ↔ LinearIndependent R v
Full source 
@[simp]
theorem LinearIndependent.group_smul_iff {G : Type*} [hG : Group G] [MulAction G R]
    [MulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : ι → M) (w : ι → G) :
    LinearIndependentLinearIndependent R (w • v) ↔ LinearIndependent R v := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩
  convert h.group_smul (fun i ↦ (w i)⁻¹)
  simp [funext_iff]
Linear Independence Equivalence under Group Scaling: $w \cdot v$ vs $v$
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $G$ a group acting on both $R$ and $M$ such that the actions are compatible via the scalar multiplication (i.e., $G$ acts as a tower of scalars and the actions commute). Given a family of vectors $v : \iota \to M$ and a family of group elements $w : \iota \to G$, the scaled family $w \cdot v$ (where $(w \cdot v)(i) = w(i) \cdot v(i)$) is linearly independent over $R$ if and only if the original family $v$ is linearly independent over $R$.
LinearIndependent.units_smul theorem
{v : ι → M} (hv : LinearIndependent R v) (w : ι → Rˣ) : LinearIndependent R (w • v)
Full source 
theorem LinearIndependent.units_smul {v : ι → M} (hv : LinearIndependent R v) (w : ι → Rˣ) :
    LinearIndependent R (w • v) := by
  rw [linearIndependent_iff''ₛ] at hv ⊢
  intro s g₁ g₂ hgs hsum i
  rw [← (w i).mul_left_inj]
  refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i
  · simp_rw [hgs i hi]
  · simpa only [smul_eq_mul, mul_smul, Pi.smul_apply'] using hsum
Linear Independence Preserved Under Scaling by Units
Informal description
Let $R$ be a ring and $M$ an $R$-module. Given a linearly independent family of vectors $v : \iota \to M$ and a family of units $w : \iota \to R^\times$, the scaled family $w \cdot v$ (defined by $(w \cdot v)(i) = w(i) \cdot v(i)$ for each $i \in \iota$) is also linearly independent over $R$.
LinearIndependent.units_smul_iff theorem
(v : ι → M) (w : ι → Rˣ) : LinearIndependent R (w • v) ↔ LinearIndependent R v
Full source 
@[simp]
theorem LinearIndependent.units_smul_iff (v : ι → M) (w : ι → Rˣ) :
    LinearIndependentLinearIndependent R (w • v) ↔ LinearIndependent R v := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩
  convert h.units_smul (fun i ↦ (w i)⁻¹)
  simp [funext_iff]
Equivalence of Linear Independence Under Unit Scaling: $w \cdot v$ is linearly independent iff $v$ is linearly independent
Informal description
Let $R$ be a ring and $M$ an $R$-module. For any family of vectors $v : \iota \to M$ and any family of units $w : \iota \to R^\times$, the scaled family $w \cdot v$ (defined by $(w \cdot v)(i) = w(i) \cdot v(i)$ for each $i \in \iota$) is linearly independent over $R$ if and only if the original family $v$ is linearly independent over $R$.
linearIndependent_span theorem
(hs : LinearIndependent R v) : LinearIndependent R (M := span R (range v)) (fun i : ι ↦ ⟨v i, subset_span (mem_range_self i)⟩)
Full source 
theorem linearIndependent_span (hs : LinearIndependent R v) :
    LinearIndependent R (M := span R (range v))
      (fun i : ι ↦ ⟨v i, subset_span (mem_range_self i)⟩) :=
  LinearIndependent.of_comp (span R (range v)).subtype hs
Linear Independence Preserved Under Span Restriction
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors in $M$. If $v$ is linearly independent over $R$, then the family of vectors obtained by restricting $v$ to the span of its range (i.e., the vectors $\langle v_i, \text{subset\_span}(\text{mem\_range\_self } i) \rangle$ for each $i \in \iota$) is also linearly independent over $R$ when viewed as vectors in $\text{span}_R(\text{range } v)$.
linearIndependent_finset_map_embedding_subtype theorem
(s : Set M) (li : LinearIndependent R ((↑) : s → M)) (t : Finset s) : LinearIndependent R ((↑) : Finset.map (Embedding.subtype s) t → M)
Full source 
/-- Every finite subset of a linearly independent set is linearly independent. -/
theorem linearIndependent_finset_map_embedding_subtype (s : Set M)
    (li : LinearIndependent R ((↑) : s → M)) (t : Finset s) :
    LinearIndependent R ((↑) : Finset.map (Embedding.subtype s) t → M) :=
  li.comp (fun _ ↦ ⟨_, _⟩) <| by intro; aesop
Finite Subsets Preserve Linear Independence Under Subtype Embedding
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $s$ a subset of $M$. If the inclusion map $s \hookrightarrow M$ is linearly independent over $R$, then for any finite subset $t$ of $s$, the inclusion map of the image of $t$ under the subtype embedding is also linearly independent over $R$.
LinearIndepOn.mono theorem
{t s : Set ι} (hs : LinearIndepOn R v s) (h : t ⊆ s) : LinearIndepOn R v t
Full source 
theorem LinearIndepOn.mono {t s : Set ι} (hs : LinearIndepOn R v s) (h : t ⊆ s) :
    LinearIndepOn R v t :=
  hs.comp _ <| Set.inclusion_injective h
Linear Independence is Preserved Under Subset Restriction
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. If the vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$ for some subset $s \subseteq \iota$, then for any subset $t \subseteq s$, the vectors $\{v_i\}_{i \in t}$ are also linearly independent over $R$.
linearIndepOn_of_finite theorem
(s : Set ι) (H : ∀ t ⊆ s, Set.Finite t → LinearIndepOn R v t) : LinearIndepOn R v s
Full source 
theorem linearIndepOn_of_finite (s : Set ι) (H : ∀ t ⊆ s, Set.Finite t → LinearIndepOn R v t) :
    LinearIndepOn R v s :=
  linearIndepOn_iffₛ.2 fun f hf g hg eq ↦
    linearIndepOn_iffₛ.1 (H _ (union_subset hf hg) <| (Finset.finite_toSet _).union <|
      Finset.finite_toSet _) f Set.subset_union_left g Set.subset_union_right eq
Finite Subsets Imply Linear Independence on Entire Set
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. For a subset $s \subseteq \iota$, if every finite subset $t \subseteq s$ is linearly independent over $R$, then the entire set $s$ is linearly independent over $R$.
LinearIndependent.disjoint_span_image theorem
(hv : LinearIndependent R v) {s t : Set ι} (hs : Disjoint s t) : Disjoint (Submodule.span R <| v '' s) (Submodule.span R <| v '' t)
Full source 
theorem LinearIndependent.disjoint_span_image (hv : LinearIndependent R v) {s t : Set ι}
    (hs : Disjoint s t) : Disjoint (Submodule.span R <| v '' s) (Submodule.span R <| v '' t) := by
  simp only [disjoint_def, Finsupp.mem_span_image_iff_linearCombination]
  rintro _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩
  rw [hv.finsuppLinearCombination_injective.eq_iff] at H; subst l₂
  have : l₁ = 0 := Submodule.disjoint_def.mp (Finsupp.disjoint_supported_supported hs) _ hl₁ hl₂
  simp [this]
Disjointness of Spans for Disjoint Sets under a Linearly Independent Map
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors. For any two disjoint subsets $s, t \subseteq \iota$, the spans of the images of $s$ and $t$ under $v$ are disjoint, i.e., $\text{span}_R (v(s)) \cap \text{span}_R (v(t)) = \{0\}$.
LinearIndependent.not_mem_span_image theorem
[Nontrivial R] (hv : LinearIndependent R v) {s : Set ι} {x : ι} (h : x ∉ s) : v x ∉ Submodule.span R (v '' s)
Full source 
theorem LinearIndependent.not_mem_span_image [Nontrivial R] (hv : LinearIndependent R v) {s : Set ι}
    {x : ι} (h : x ∉ s) : v x ∉ Submodule.span R (v '' s) := by
  have h' : v x ∈ Submodule.span R (v '' {x}) := by
    rw [Set.image_singleton]
    exact mem_span_singleton_self (v x)
  intro w
  apply LinearIndependent.ne_zero x hv
  refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w
  simpa using h
Linear Independence Implies Non-Membership in Span of Disjoint Image
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors. For any subset $s \subseteq \iota$ and any element $x \in \iota$ such that $x \notin s$, the vector $v(x)$ does not belong to the span of the image of $s$ under $v$, i.e., $v(x) \notin \text{span}_R (v(s))$.
LinearIndependent.linearCombination_ne_of_not_mem_support theorem
[Nontrivial R] (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) : f.linearCombination R v ≠ v x
Full source 
theorem LinearIndependent.linearCombination_ne_of_not_mem_support [Nontrivial R]
    (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) :
    f.linearCombination R v ≠ v x := by
  replace h : x ∉ (f.support : Set ι) := h
  intro w
  have p : ∀ x ∈ Finsupp.supported R R f.support,
    Finsupp.linearCombination R v x ≠ f.linearCombination R v := by
    simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.not_mem_span_image h
  exact p f (f.mem_supported_support R) rfl
Non-Equality of Linear Combination and Basis Vector Outside Support
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors. For any finitely supported function $f : \iota \to_{\text{f}} R$ and any element $x \in \iota$ not in the support of $f$, the linear combination $\sum_{i \in \text{supp}(f)} f(i) \cdot v(i)$ is not equal to $v(x)$.
LinearIndepOn.id_imageₛ theorem
{s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Set.InjOn f (span R s)) : LinearIndepOn R id (f '' s)
Full source 
theorem LinearIndepOn.id_imageₛ {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s)
    (hf_inj : Set.InjOn f (span R s)) : LinearIndepOn R id (f '' s) :=
  id_image <| hs.map_injOn f (by simpa using hf_inj)
Preservation of Linear Independence under Injective Linear Maps on Span
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $s \subseteq M$ be a subset. If the identity function $\text{id} : M \to M$ is linearly independent on $s$ over $R$ (i.e., the vectors in $s$ are linearly independent), and $f : M \to M'$ is a linear map that is injective on the span of $s$, then the identity function $\text{id} : M' \to M'$ is linearly independent on the image $f(s)$ over $R$ (i.e., the vectors in $f(s)$ are linearly independent).
surjective_of_linearIndependent_of_span theorem
[Nontrivial R] (hv : LinearIndependent R v) (f : ι' ↪ ι) (hss : range v ⊆ span R (range (v ∘ f))) : Surjective f
Full source 
theorem surjective_of_linearIndependent_of_span [Nontrivial R] (hv : LinearIndependent R v)
    (f : ι' ↪ ι) (hss : rangerange v ⊆ span R (range (v ∘ f))) : Surjective f := by
  intro i
  let repr : (span R (range (v ∘ f)) : Type _) → ι' →₀ R := (hv.comp f f.injective).repr
  let l := (repr ⟨v i, hss (mem_range_self i)⟩).mapDomain f
  have h_total_l : Finsupp.linearCombination R v l = v i := by
    dsimp only [l]
    rw [Finsupp.linearCombination_mapDomain]
    rw [(hv.comp f f.injective).linearCombination_repr]
  have h_total_eq : Finsupp.linearCombination R v l = Finsupp.linearCombination R v
       (Finsupp.single i 1) := by
    rw [h_total_l, Finsupp.linearCombination_single, one_smul]
  have l_eq : l = _ := hv h_total_eq
  dsimp only [l] at l_eq
  rw [← Finsupp.embDomain_eq_mapDomain] at l_eq
  rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨i', hi'⟩
  use i'
  exact hi'.2
Surjectivity of Index Function for Span-Preserving Linear Independence
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, and $v : \iota \to M$ a linearly independent family of vectors. Given an injective function $f : \iota' \hookrightarrow \iota$ such that the range of $v$ is contained in the span of the range of $v \circ f$, then $f$ is surjective.
le_of_span_le_span theorem
[Nontrivial R] {s t u : Set M} (hl : LinearIndepOn R id u) (hsu : s ⊆ u) (htu : t ⊆ u) (hst : span R s ≤ span R t) : s ⊆ t
Full source 
theorem le_of_span_le_span [Nontrivial R] {s t u : Set M} (hl : LinearIndepOn R id u)
    (hsu : s ⊆ u) (htu : t ⊆ u) (hst : span R s ≤ span R t) : s ⊆ t := by
  have :=
    eq_of_linearIndepOn_id_of_span_subtype (hl.mono (Set.union_subset hsu htu))
      Set.subset_union_right (Set.union_subset (Set.Subset.trans subset_span hst) subset_span)
  rw [← this]; apply Set.subset_union_left
Span containment implies subset containment for linearly independent sets
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, and $u \subseteq M$ a linearly independent set. For any subsets $s, t \subseteq u$, if the span of $s$ is contained in the span of $t$ (i.e., $\text{span}_R s \leq \text{span}_R t$), then $s$ is a subset of $t$ (i.e., $s \subseteq t$).
span_le_span_iff theorem
[Nontrivial R] {s t u : Set M} (hl : LinearIndependent R ((↑) : u → M)) (hsu : s ⊆ u) (htu : t ⊆ u) : span R s ≤ span R t ↔ s ⊆ t
Full source 
theorem span_le_span_iff [Nontrivial R] {s t u : Set M} (hl : LinearIndependent R ((↑) : u → M))
    (hsu : s ⊆ u) (htu : t ⊆ u) : spanspan R s ≤ span R t ↔ s ⊆ t :=
  ⟨le_of_span_le_span hl hsu htu, span_mono⟩
Span containment equivalence for linearly independent sets
Informal description
Let $R$ be a nontrivial ring, $M$ an $R$-module, and $u \subseteq M$ a linearly independent set. For any subsets $s, t \subseteq u$, the span of $s$ is contained in the span of $t$ if and only if $s$ is a subset of $t$, i.e., \[ \text{span}_R s \leq \text{span}_R t \leftrightarrow s \subseteq t. \]
LinearIndependent.map theorem
(hv : LinearIndependent R v) {f : M →ₗ[R] M'} (hf_inj : Disjoint (span R (range v)) (LinearMap.ker f)) : LinearIndependent R (f ∘ v)
Full source 
/-- If `v` is a linearly independent family of vectors and the kernel of a linear map `f` is
disjoint with the submodule spanned by the vectors of `v`, then `f ∘ v` is a linearly independent
family of vectors. See also `LinearIndependent.map'` for a special case assuming `ker f = ⊥`. -/
theorem LinearIndependent.map (hv : LinearIndependent R v) {f : M →ₗ[R] M'}
    (hf_inj : Disjoint (span R (range v)) (LinearMap.ker f)) : LinearIndependent R (f ∘ v) :=
  (f.linearIndependent_iff_of_disjoint hf_inj).mpr hv
Preservation of Linear Independence Under Linear Maps with Disjoint Kernel
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a linearly independent family of vectors. Given a linear map $f : M \to M'$ such that the span of the range of $v$ is disjoint from the kernel of $f$, then the composition $f \circ v : \iota \to M'$ is also a linearly independent family of vectors.
LinearIndependent.map' theorem
(hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) : LinearIndependent R (f ∘ v)
Full source 
/-- An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also `LinearIndependent.map` for a more general statement. -/
theorem LinearIndependent.map' (hv : LinearIndependent R v) (f : M →ₗ[R] M')
    (hf_inj : LinearMap.ker f = ⊥) : LinearIndependent R (f ∘ v) :=
  hv.map <| by simp_rw [hf_inj, disjoint_bot_right]
Preservation of Linear Independence Under Injective Linear Maps
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a linearly independent family of vectors. Given an injective linear map $f : M \to M'$ (i.e., $\ker f = \{0\}$), then the composition $f \circ v : \iota \to M'$ is also a linearly independent family of vectors.
LinearIndependent.map_of_injective_injective theorem
{R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M'] (hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : ∀ m, j m = 0 → m = 0) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (j ∘ v)
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map, `j : M →+ M'` is a monoid map,
such that they send non-zero elements to non-zero elements, and compatible with the scalar
multiplications on `M` and `M'`, then `j` sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map'`. -/
theorem LinearIndependent.map_of_injective_injective {R' M' : Type*}
    [Ring R'] [AddCommGroup M'] [Module R' M'] (hv : LinearIndependent R v)
    (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : ∀ m, j m = 0 → m = 0)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (j ∘ v) := by
  rw [linearIndependent_iff'] at hv ⊢
  intro S r' H s hs
  simp_rw [comp_apply, ← hc, ← map_sum] at H
  exact hi _ <| hv _ _ (hj _ H) s hs
Preservation of Linear Independence Under Compatible Ring and Module Homomorphisms
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M'$ an $R'$-module. Given a linearly independent family of vectors $v : \iota \to M$ over $R$, a ring homomorphism $i : R' \to R$ that sends non-zero elements to non-zero elements, and an additive monoid homomorphism $j : M \to M'$ that sends non-zero elements to non-zero elements, if $j$ satisfies the compatibility condition $j(i(r) \cdot m) = r \cdot j(m)$ for all $r \in R'$ and $m \in M$, then the composed family $j \circ v : \iota \to M'$ is linearly independent over $R'$.
LinearIndependent.map_of_surjective_injective theorem
{R' M' : Type*} [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v) (i : R → R') (j : M →+ M') (hi : Surjective i) (hj : ∀ m, j m = 0 → m = 0) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v)
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map which maps zero to zero,
`j : M →+ M'` is a monoid map which sends non-zero elements to non-zero elements, such that the
scalar multiplications on `M` and `M'` are compatible, then `j` sends linearly independent families
of vectors to linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map'`. -/
theorem LinearIndependent.map_of_surjective_injective {R' M' : Type*}
    [Semiring R'] [AddCommMonoid M'] [Module R' M'] (hv : LinearIndependent R v)
    (i : R → R') (j : M →+ M') (hi : Surjective i) (hj : ∀ m, j m = 0 → m = 0)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v) :=
  hv.map_of_surjective_injectiveₛ i _ hi ((injective_iff_map_eq_zero _).mpr hj) hc
Preservation of Linear Independence under Surjective Ring and Injective Module Homomorphisms
Informal description
Let $R$ and $R'$ be semirings, and let $M$ be an $R$-module and $M'$ an $R'$-module. Given a linearly independent family of vectors $v : \iota \to M$ over $R$, a surjective ring homomorphism $i : R \to R'$, and an additive monoid homomorphism $j : M \to M'$ that sends only the zero element to zero, if $j$ satisfies the compatibility condition $j(r \cdot m) = i(r) \cdot j(m)$ for all $r \in R$ and $m \in M$, then the composed family $j \circ v : \iota \to M'$ is linearly independent over $R'$.
LinearMap.linearIndependent_iff theorem
(f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) : LinearIndependent R (f ∘ v) ↔ LinearIndependent R v
Full source 
/-- If `f` is an injective linear map, then the family `f ∘ v` is linearly independent
if and only if the family `v` is linearly independent. -/
protected theorem LinearMap.linearIndependent_iff (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) :
    LinearIndependentLinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
  f.linearIndependent_iff_of_disjoint <| by simp_rw [hf_inj, disjoint_bot_right]
Linear Independence Preservation Under Injective Linear Maps
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $v : \iota \to M$ be a family of vectors. Given an injective linear map $f : M \to M'$ (i.e., $\ker f = \{0\}$), the family $f \circ v$ is linearly independent over $R$ if and only if the family $v$ is linearly independent over $R$.
LinearIndependent.fin_cons' theorem
{m : ℕ} (x : M) (v : Fin m → M) (hli : LinearIndependent R v) (x_ortho : ∀ (c : R) (y : Submodule.span R (Set.range v)), c • x + y = (0 : M) → c = 0) : LinearIndependent R (Fin.cons x v : Fin m.succ → M)
Full source 
/-- See `LinearIndependent.fin_cons` for a family of elements in a vector space. -/
theorem LinearIndependent.fin_cons' {m : ℕ} (x : M) (v : Fin m → M) (hli : LinearIndependent R v)
    (x_ortho : ∀ (c : R) (y : Submodule.span R (Set.range v)), c • x + y = (0 : M) → c = 0) :
    LinearIndependent R (Fin.cons x v : Fin m.succ → M) := by
  rw [Fintype.linearIndependent_iff] at hli ⊢
  rintro g total_eq j
  simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq
  have : g 0 = 0 := by
    refine x_ortho (g 0) ⟨∑ i : Fin m, g i.succ • v i, ?_⟩ total_eq
    exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)
  rw [this, zero_smul, zero_add] at total_eq
  exact Fin.cases this (hli _ total_eq) j
Linear Independence Preservation Under Finitary Extension with Orthogonal Vector
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \text{Fin} m \to M$ a linearly independent family of vectors. Given a vector $x \in M$ such that for any scalar $c \in R$ and any vector $y$ in the span of $v$, the equation $c \cdot x + y = 0$ implies $c = 0$, then the extended family $\text{Fin.cons}(x, v) : \text{Fin} (m+1) \to M$ is also linearly independent.
linearIndependent_sum theorem
{v : ι ⊕ ι' → M} : LinearIndependent R v ↔ LinearIndependent R (v ∘ Sum.inl) ∧ LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (Submodule.span R (range (v ∘ Sum.inl))) (Submodule.span R (range (v ∘ Sum.inr)))
Full source 
theorem linearIndependent_sum {v : ι ⊕ ι' → M} :
    LinearIndependentLinearIndependent R v ↔
      LinearIndependent R (v ∘ Sum.inl) ∧
        LinearIndependent R (v ∘ Sum.inr) ∧
          Disjoint (Submodule.span R (range (v ∘ Sum.inl)))
            (Submodule.span R (range (v ∘ Sum.inr))) := by
  classical
  rw [range_comp v, range_comp v]
  refine ⟨?_, ?_⟩
  · intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint
  rintro ⟨hl, hr, hlr⟩
  rw [linearIndependent_iff'] at *
  intro s g hg i hi
  have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 := by
    -- Porting note: `g` must be specified.
    rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_True]
    · exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
  rw [← eq_neg_iff_add_eq_zero] at this
  rw [disjoint_def'] at hlr
  have A := by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
  rcases i with i | i
  · exact hl _ _ A i (Finset.mem_preimage.2 hi)
  · rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)
Linear Independence of Sum Family via Component Independence and Disjoint Spans
Informal description
A family of vectors $v : \iota \oplus \iota' \to M$ is linearly independent over a ring $R$ if and only if the following three conditions hold: 1. The restriction $v \circ \text{inl} : \iota \to M$ is linearly independent, 2. The restriction $v \circ \text{inr} : \iota' \to M$ is linearly independent, and 3. The spans of the ranges of $v \circ \text{inl}$ and $v \circ \text{inr}$ are disjoint, i.e., $\text{span}_R(\text{range}(v \circ \text{inl})) \cap \text{span}_R(\text{range}(v \circ \text{inr})) = \{0\}$.
LinearIndependent.sum_type theorem
{v' : ι' → M} (hv : LinearIndependent R v) (hv' : LinearIndependent R v') (h : Disjoint (Submodule.span R (range v)) (Submodule.span R (range v'))) : LinearIndependent R (Sum.elim v v')
Full source 
theorem LinearIndependent.sum_type {v' : ι' → M} (hv : LinearIndependent R v)
    (hv' : LinearIndependent R v')
    (h : Disjoint (Submodule.span R (range v)) (Submodule.span R (range v'))) :
    LinearIndependent R (Sum.elim v v') :=
  linearIndependent_sum.2 ⟨hv, hv', h⟩
Linear Independence of Combined Sum Family via Component Independence and Disjoint Spans
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$, $v' : \iota' \to M$ be two families of vectors. If: 1. $v$ is linearly independent over $R$, 2. $v'$ is linearly independent over $R$, and 3. The spans of the ranges of $v$ and $v'$ are disjoint, i.e., $\text{span}_R(\text{range}(v)) \cap \text{span}_R(\text{range}(v')) = \{0\}$, then the combined family $\text{Sum.elim}\,v\,v' : \iota \oplus \iota' \to M$ is linearly independent over $R$.
LinearIndepOn.union theorem
{t : Set ι} (hs : LinearIndepOn R v s) (ht : LinearIndepOn R v t) (hdj : Disjoint (span R (v '' s)) (span R (v '' t))) : LinearIndepOn R v (s ∪ t)
Full source 
theorem LinearIndepOn.union {t : Set ι} (hs : LinearIndepOn R v s) (ht : LinearIndepOn R v t)
    (hdj : Disjoint (span R (v '' s)) (span R (v '' t))) : LinearIndepOn R v (s ∪ t) := by
  nontriviality R
  classical
  have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
  have hdj := (hdj.of_span₀ hs.zero_not_mem_image).of_image
  rw [LinearIndepOn]
  convert (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
  · rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
  rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
Linear Independence Preserved Under Union of Disjoint Span Subfamilies
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. For any subsets $s, t \subseteq \iota$, if: 1. The vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$, 2. The vectors $\{v_i\}_{i \in t}$ are linearly independent over $R$, and 3. The spans of the images $v(s)$ and $v(t)$ are disjoint, i.e., $\text{span}_R(v(s)) \cap \text{span}_R(v(t)) = \{0\}$, then the vectors $\{v_i\}_{i \in s \cup t}$ are linearly independent over $R$.
LinearIndepOn.id_union theorem
{s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t) (hdj : Disjoint (span R s) (span R t)) : LinearIndepOn R id (s ∪ t)
Full source 
theorem LinearIndepOn.id_union {s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t)
    (hdj : Disjoint (span R s) (span R t)) : LinearIndepOn R id (s ∪ t) :=
  hs.union ht (by simpa)
Linear Independence Preserved Under Union of Disjoint Span Subsets
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $s, t \subseteq M$ subsets of vectors. If: 1. The vectors in $s$ are linearly independent over $R$ (when considered as a family via the identity map), 2. The vectors in $t$ are linearly independent over $R$ (when considered as a family via the identity map), and 3. The spans of $s$ and $t$ are disjoint, i.e., $\text{span}_R(s) \cap \text{span}_R(t) = \{0\}$, then the vectors in $s \cup t$ are linearly independent over $R$ (when considered as a family via the identity map).
linearIndepOn_union_iff theorem
{t : Set ι} (hdj : Disjoint s t) : LinearIndepOn R v (s ∪ t) ↔ LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t))
Full source 
theorem linearIndepOn_union_iff {t : Set ι} (hdj : Disjoint s t) :
    LinearIndepOnLinearIndepOn R v (s ∪ t) ↔
    LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t)) := by
  refine ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩,
    fun h ↦ h.1.union h.2.1 h.2.2⟩
  convert h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _) <;>
  aesop
Characterization of Linear Independence for Union of Disjoint Sets
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $v : \iota \to M$ a family of vectors. For any disjoint subsets $s, t \subseteq \iota$, the vectors $\{v_i\}_{i \in s \cup t}$ are linearly independent over $R$ if and only if: 1. The vectors $\{v_i\}_{i \in s}$ are linearly independent over $R$, 2. The vectors $\{v_i\}_{i \in t}$ are linearly independent over $R$, and 3. The spans of the images $v(s)$ and $v(t)$ are disjoint, i.e., $\text{span}_R(v(s)) \cap \text{span}_R(v(t)) = \{0\}$.
linearIndepOn_id_union_iff theorem
{s t : Set M} (hdj : Disjoint s t) : LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)
Full source 
theorem linearIndepOn_id_union_iff {s t : Set M} (hdj : Disjoint s t) :
    LinearIndepOnLinearIndepOn R id (s ∪ t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t) := by
  rw [linearIndepOn_union_iff hdj, image_id, image_id]
Characterization of Linear Independence for Union of Disjoint Sets via Identity Map
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $s, t \subseteq M$ disjoint subsets. The vectors in $s \cup t$ are linearly independent over $R$ (when considered via the identity map) if and only if: 1. The vectors in $s$ are linearly independent over $R$, 2. The vectors in $t$ are linearly independent over $R$, and 3. The spans of $s$ and $t$ are disjoint, i.e., $\text{span}_R(s) \cap \text{span}_R(t) = \{0\}$.
LinearIndepOn.image theorem
{s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Disjoint (span R s) (LinearMap.ker f)) : LinearIndepOn R id (f '' s)
Full source 
theorem LinearIndepOn.image {s : Set M} {f : M →ₗ[R] M'}
    (hs : LinearIndepOn R id s) (hf_inj : Disjoint (span R s) (LinearMap.ker f)) :
    LinearIndepOn R id (f '' s) :=
  hs.id_imageₛ <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj
Preservation of Linear Independence under Linear Maps with Disjoint Kernel
Informal description
Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $s \subseteq M$ be a subset. If the vectors in $s$ are linearly independent over $R$ (i.e., $\text{LinearIndepOn}_R \text{id} s$ holds), and $f : M \to M'$ is a linear map such that the span of $s$ is disjoint from the kernel of $f$, then the image $f(s) \subseteq M'$ is also linearly independent over $R$.
linearIndependent_monoidHom theorem
(G : Type*) [MulOneClass G] (L : Type*) [CommRing L] [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L)
Full source 
/-- Dedekind's linear independence of characters -/
@[stacks 0CKL]
theorem linearIndependent_monoidHom (G : Type*) [MulOneClass G] (L : Type*) [CommRing L]
    [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L) := by
  -- Porting note: Some casts are required.
  letI := Classical.decEq (G →* L)
  letI : MulAction L L := DistribMulAction.toMulAction
  -- We prove linear independence by showing that only the trivial linear combination vanishes.
  apply linearIndependent_iff'.2
  intro s
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
  intro g hg
  -- Here
  -- * `a` is a new character we will insert into the `Finset` of characters `s`,
  -- * `ih` is the fact that only the trivial linear combination of characters in `s` is zero
  -- * `hg` is the fact that `g` are the coefficients of a linear combination summing to zero
  -- and it remains to prove that `g` vanishes on `insert a s`.
  -- We now make the key calculation:
  -- For any character `i` in the original `Finset`, we have `g i • i = g i • a` as functions
  -- on the monoid `G`.
  have h1 (i) (his : i ∈ s) : (g i • (i : G → L)) = g i • (a : G → L) := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, ((g i * i x - g i * a x) • (i : G → L))) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, (g i • (i : G → L))) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp
  -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
  -- there is some element of the monoid on which it differs from `a`.
  have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
    by_contra! hia
    obtain rfl : i = a := MonoidHom.ext hia
    contradiction
  -- From these two facts we deduce that `g` actually vanishes on `s`,
  have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)
  -- And so, using the fact that the linear combination over `s` and over `insert a s` both
  -- vanish, we deduce that `g a = 0`.
  have h4 : g a = 0 :=
    calc
      g a = g a * 1 := (mul_one _).symm
      _ = (g a • (a : G → L)) 1 := by rw [← a.map_one]; rfl
      _ = (∑ i ∈ insert a s, (g i • (i : G → L))) 1 := by
        rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]
      _ = 0 := by rw [hg]; rfl
  -- Now we're done; the last two facts together imply that `g` vanishes on every element
  -- of `insert a s`.
  exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩
Linear Independence of Monoid Homomorphisms (Dedekind's Theorem)
Informal description
Let $G$ be a monoid and $L$ be a commutative ring with no zero divisors. Then the set of monoid homomorphisms from $G$ to $L$, considered as vectors in the function space $G \to L$, is linearly independent over $L$.
linearIndependent_unique_iff theorem
(v : ι → M) [Unique ι] : LinearIndependent R v ↔ v default ≠ 0
Full source 
theorem linearIndependent_unique_iff (v : ι → M) [Unique ι] :
    LinearIndependentLinearIndependent R v ↔ v default ≠ 0 := by
  simp only [linearIndependent_iff, Finsupp.linearCombination_unique, smul_eq_zero]
  refine ⟨fun h hv => ?_, fun hv l hl => Finsupp.unique_ext <| hl.resolve_right hv⟩
  have := h (Finsupp.single default 1) (Or.inr hv)
  exact one_ne_zero (Finsupp.single_eq_zero.1 this)
Linear independence criterion for families indexed by a unique type: $v$ is linearly independent if and only if $v(\text{default}) \neq 0$
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $\iota$ a type with a unique element. A family of vectors $v \colon \iota \to M$ is linearly independent over $R$ if and only if $v(\text{default}) \neq 0$, where $\text{default}$ is the unique element of $\iota$.
linearIndepOn_singleton_iff theorem
{i : ι} {v : ι → M} : LinearIndepOn R v { i } ↔ v i ≠ 0
Full source 
@[simp]
theorem linearIndepOn_singleton_iff {i : ι} {v : ι → M} : LinearIndepOnLinearIndepOn R v {i} ↔ v i ≠ 0 :=
  ⟨fun h ↦ h.ne_zero rfl, fun h ↦ linearIndependent_unique _ h⟩
Linear Independence Criterion for Singleton Families: $\{v_i\}$ is linearly independent if and only if $v_i \neq 0$
Informal description
For a family of vectors $v \colon \iota \to M$ over a ring $R$ and an index $i \in \iota$, the vectors $\{v_i\}$ are linearly independent over $R$ if and only if $v_i \neq 0$.
LinearIndepOn.id_singleton theorem
{x : M} (hx : x ≠ 0) : LinearIndepOn R id { x }
Full source 
theorem LinearIndepOn.id_singleton {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x} :=
  linearIndependent_unique Subtype.val hx
Linear Independence of Singleton Sets via Identity Map: $\{x\}$ is linearly independent if $x \neq 0$
Informal description
For any nonzero vector $x$ in an $R$-module $M$, the singleton set $\{x\}$ is linearly independent over $R$ when considered as a family via the identity map.
linearIndependent_subsingleton_index_iff theorem
[Subsingleton ι] (f : ι → M) : LinearIndependent R f ↔ ∀ i, f i ≠ 0
Full source 
@[simp]
theorem linearIndependent_subsingleton_index_iff [Subsingleton ι] (f : ι → M) :
    LinearIndependentLinearIndependent R f ↔ ∀ i, f i ≠ 0 := by
  obtain (he | he) := isEmpty_or_nonempty ι
  · simp [linearIndependent_empty_type]
  obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩
  rw [linearIndependent_unique_iff]
  exact ⟨fun h i ↦ by rwa [Unique.eq_default i], fun h ↦ h _⟩
Linear independence criterion for families indexed by a subsingleton type: $f$ is linearly independent if and only if all $f(i) \neq 0$
Informal description
Let $R$ be a ring, $M$ an $R$-module, and $\iota$ a type with at most one element (a subsingleton). A family of vectors $f \colon \iota \to M$ is linearly independent over $R$ if and only if for every $i \in \iota$, the vector $f(i)$ is nonzero.
linearIndependent_subsingleton_iff theorem
[Subsingleton M] (f : ι → M) : LinearIndependent R f ↔ IsEmpty ι
Full source 
@[simp]
theorem linearIndependent_subsingleton_iff [Subsingleton M] (f : ι → M) :
    LinearIndependentLinearIndependent R f ↔ IsEmpty ι := by
  obtain h | i := isEmpty_or_nonempty ι
  · simpa
  exact iff_of_false (fun hli ↦ hli.ne_zero i.some (Subsingleton.eq_zero (f i.some))) (by simp)
Linear Independence in Subsingleton Modules iff Index Type is Empty
Informal description
For a subsingleton module $M$ (i.e., a module with at most one element) and any family of vectors $f : \iota \to M$, the family $f$ is linearly independent over $R$ if and only if the index type $\iota$ is empty.