Commit 2023-08-22 03:35 8f782305

View on Github →

feat: compute rank of and as -modules (#6672) This adds a trivial cardinality argument that shows that when V is a free K-module where K is infinite and satisfies the strong rank condiiton, then the rank of V coincides with its cardinality. This is then used to establish that Module.rank ℚ ℝ = continuum = Module.rank ℚ ℂ, and therefore that and are isomorphic as vector spaces over . As requested on Zulip

Estimated changes