Theorems · Definition · linear algebra

LinearMap.BilinForm.dualBasis

{V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {ι : Type u_9} →
            [DecidableEq ι] →
              [Finite ι] → (B : LinearMap.BilinForm K V) → B.Nondegenerate → Module.Basis ι K V → Module.Basis ι K V

The B-dual basis B.dualBasis hB b to a finite basis b satisfies B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0, where B is a nondegenerate (symmetric) bilinear form and b is a finite basis.

Defined in

Mathlib.LinearAlgebra.BilinearForm.Properties

Cited by

20 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleDecidableEqFinite