Theorems · Definition · linear algebra

basisOfPiSpaceOfLinearIndependent

{K : Type u} →
  [inst : DivisionRing K] →
    {ι : Type u_1} →
      [Fintype ι] → [Decidable (Nonempty ι)] → {b : ι → ι → K} → LinearIndependent K b → Module.Basis ι K (ι → K)

In a vector space ι → K, a linear independent family indexed by ι is a basis.

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Cited by

4 results in Mathlib

Foundations

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

Assumes

DivisionRingFintypeDecidable