Duality

AbbreviationDual vector space#

The left dual space of an R-module M is the R-module of linear maps M → R.

Module.Dual.{u_3, u_4} (R : Type u_3) (M : Type u_4) [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] : Type (max u_4 u_3)

Sources

• Mathlib documentation: Module.Dual
• Source of Module.Dual in Mathlib/LinearAlgebra/Dual/Defs.lean
• Mathlib overview: Linear algebra › Duality
• Mathlib undergraduate list: Linear algebra › Duality

MathlibModule.Dual

Uses 1 · Used by 8

Statement usesLinear map

Used byHahn-Banach theorem · Maximal tensor product · Dual basis · Isomorphism with bidual · Lie's theorem · Adjoint endomorphism · Orthogonality · Transpose of a linear map

DefinitionDual basis#

Maps a basis for V to a basis for the dual space.

Module.Basis.dualBasis.{uR, uM, uι} {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R]
  [AddCommMonoid M] [_root_.Module R M] [DecidableEq ι] (b : Module.Basis ι R M) [Finite ι] :
  Module.Basis ι R (Module.Dual R M)

Sources

• Mathlib documentation: Module.Basis.dualBasis
• Source of Module.Basis.dualBasis in Mathlib/LinearAlgebra/Dual/Basis.lean
• Mathlib overview: Linear algebra › Duality
• Mathlib undergraduate list: Linear algebra › Duality

MathlibModule.Basis.dualBasis

Uses 3

Statement usesBasis · Dual vector space · Range of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.