Theorems · Theorem · linear algebra

Module.le_rank_iff_exists_finset

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Note: if the rank of a module is infinite, it may not contain a linear independent subset with cardinality equal to the rank, see https://mathoverflow.net/questions/263020/maximum-cardinal-of-a-set-of-linearly-independent-vectors-in-a-module.

Defined in

Mathlib.LinearAlgebra.Dimension.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleNontrivial