Commit 2023-08-22 03:35 8f782305

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