Theorems · Theorem · linear algebra

iSupIndep.linearIndependent

∀ {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] [IsDomain R]
  [Module.IsTorsionFree R N] {ι : Type u_7} (p : ι → Submodule R N),
  iSupIndep p → ∀ {v : ι → N}, (∀ (i : ι), v i ∈ p i) → (∀ (i : ι), v i ≠ 0) → LinearIndependent R v

If a family of submodules is independent, then a choice of nonzero vector from each submodule forms a linearly independent family. See also iSupIndep.linearIndependent'.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

4 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleIsDomainModule.IsTorsionFree