Theorems · Definition · commutative algebra

Module.Free.chooseBasis

(R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Free R M] → Module.Basis (Module.Free.ChooseBasisIndex R M) R M

If Module.Free R M then chooseBasis : ι → M is the basis. Here ι = ChooseBasisIndex R M.

Defined in

Mathlib.LinearAlgebra.FreeModule.Basic

Cited by

121 results in Mathlib

Foundations

Depth 87 from the axioms, rests on 1,799 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleModule.Free