toDualEquiv — Mathlib

English

A vector space is linearly isomorphic to its dual via a basis; toDualEquiv provides a linear equivalence M ≃ M*.

Русский

Векторное пространство линейно эквивалентно своему дуальному пространству через базис; toDualEquiv задаёт линейное эквивалентность M ≃ M*.

LaTeX

$$$ toDualEquiv : M \simeq_{R} Dual(R) M. $$$

Lean4

/-- A vector space is linearly equivalent to its dual space. -/
def toDualEquiv : M ≃ₗ[R] Dual R M :=
  .ofBijective b.toDual
    ⟨b.toDual_injective, range_eq_top.mp b.toDual_range⟩
      -- `simps` times out when generating this

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