Theorems · Definition · linear algebra

Module.Basis.toDual

{R : Type uR} →
  {M : Type uM} →
    {ι : Type uι} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [DecidableEq ι] → Module.Basis ι R M → M →ₗ[R] Module.Dual R M

The linear map from a vector space equipped with basis to its dual vector space, taking basis elements to corresponding dual basis elements.

Defined in

Mathlib.LinearAlgebra.Dual.Basis

Cited by

18 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleDecidableEq