Theorems · Definition · linear algebra

coevaluation

(K : Type u) →
  [inst : Field K] →
    (V : Type v) →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → K →ₗ[K] TensorProduct K V (Module.Dual K V)

The coevaluation map is a linear map from a field K to a finite-dimensional vector space V.

Defined in

Mathlib.LinearAlgebra.Coevaluation

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleFiniteDimensional