Duality

• Dual vector space
• Dual basis

DefinitionTranspose of a linear map#

The transposition of linear maps, as a linear map from M →ₗ[R] M' to Dual R M' →ₗ[R] Dual R M.

Module.Dual.transpose.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} [CommSemiring R]
  [AddCommMonoid M] [_root_.Module R M] {M' : Type u_3} [AddCommMonoid M'] [_root_.Module R M'] :
  (M →ₗ[R] M') →ₗ[R] Module.Dual R M' →ₗ[R] Module.Dual R M

Sources

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

MathlibModule.Dual.transpose

Uses 1

Statement usesDual vector space

DefinitionOrthogonality#

The dualAnnihilator of a submodule W is the set of linear maps φ such that φ w = 0 for all w ∈ W.

Submodule.dualAnnihilator.{u_3, u_4} {R : Type u_3} {M : Type u_4} [CommSemiring R]
  [AddCommMonoid M] [_root_.Module R M] (W : Submodule R M) : Submodule R (Module.Dual R M)

Sources

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

MathlibSubmodule.dualAnnihilator

Uses 2

Statement usesDual vector space · Kernel of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.