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