Theorems · Definition · linear algebra

LinearMap.BilinForm.toDual

{V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] → (B : LinearMap.BilinForm K V) → B.Nondegenerate → V ≃ₗ[K] Module.Dual K V

Given a nondegenerate bilinear form B on a finite-dimensional vector space, B.toDual is the linear equivalence between a vector space and its dual.

Defined in

Mathlib.LinearAlgebra.BilinearForm.Properties

Cited by

7 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleFiniteDimensional