Theorems · Definition · linear algebra

Module.Basis.exteriorPower

{R : Type u_1} →
  {M : Type u_3} →
    (n : ℕ) →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {I : Type u_5} → [LinearOrder I] → Module.Basis I R M → Module.Basis (↑(Set.powersetCard I n)) R ↥(⋀[R]^n M)

If b is a basis of M (indexed by a linearly ordered type), the basis of the nth exterior power of M formed by the n-fold exterior products of elements of b.

Defined in

Mathlib.LinearAlgebra.ExteriorPower.Basis

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleLinearOrder