Theorems · Definition · functional analysis

OrthonormalBasis.exteriorPower

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [inst_2 : FiniteDimensional ℝ E] →
        {I : Type u_2} →
          [inst_3 : Fintype I] →
            [LinearOrder I] → OrthonormalBasis I ℝ E → (n : ℕ) → OrthonormalBasis ↑(Set.powersetCard I n) ℝ ↥(⋀[ℝ]^n E)

An orthonormal basis of a finite-dimensional real inner product space E induces an orthonormal basis of ⋀[ℝ]^n E, indexed by n-element subsets of the index type.

Defined in

Mathlib.Analysis.InnerProductSpace.ExteriorPower

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalFintypeLinearOrder