Theorems · Definition · linear algebra

basisOfLinearIndependentOfCardEqFinrank

{K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {ι : Type u_1} →
            [inst_3 : Fintype ι] →
              [Nonempty ι] →
                {b : ι → V} → LinearIndependent K b → Fintype.card ι = Module.finrank K V → Module.Basis ι K V

A linear independent family of finrank K V vectors forms a basis.

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleFintypeNonempty