dualBasis — Mathlib

English

Given a basis b, the dualBasis for the dual space is defined as the image of b under the isomorphism toDualEquiv: dualBasis := b.map b.toDualEquiv.

Русский

Для данного базиса b дуальная база для дуального пространства определяется как образ b через изоморфизм toDualEquiv: dualBasis := b.map b.toDualEquiv.

LaTeX

$$$ dualBasis : Basis ι R (Dual R M) := b.map b.toDualEquiv. $$$

Lean4

/-- Maps a basis for `V` to a basis for the dual space. -/
def dualBasis : Basis ι R (Dual R M) :=
  b.map b.toDualEquiv

Похожие утверждения