Theorems · Theorem · linear algebra

Basis.linearEquiv_dual_iff_finiteDimensional

∀ {K : Type uK} {V : Type uV} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V

A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional: a consequence of the Erdős-Kaplansky theorem.

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModule