Theorems · Definition · linear algebra

Subspace.dualLift

{K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (W : Subspace K V) → Module.Dual K ↥W →ₗ[K] Module.Dual K V

Given a subspace W of V and an element of its dual φ, dualLift W φ is an arbitrary extension of φ to an element of the dual of V. That is, dualLift W φ sends w ∈ W to φ x and x in a chosen complement of W to 0.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

9 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModule