Commit 2023-12-27 19:55 04a04880

feat(LinearAlgebra): the Erdős-Kaplansky theorem (#9159) The dimension of an infinite dimensional dual space is equal to its cardinality. As a consequence (linearEquiv_dual_iff_finiteDimensional), a vector space is isomorphic to its dual iff it's finite dimensional. The main argument is from https://mathoverflow.net/a/168624. There is a slicker proof in the field case but Vandermonde determinants don't work in a non-commutative ring. Resolves TODO item posed by Julian Külshammer

• depends on: #8941
• depends on: #8942