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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Hamel.20basis.20and.20reals.20isomorphic.20to.20the.20complexes.20as.20an.20a.2E.2E.2E)

Mathlib/Data/Complex/Module.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Sébastien Gouëzel, Eric Wieser
 -/
 import Mathlib.Algebra.Order.SMul
-import Mathlib.Data.Complex.Basic
+import Mathlib.Data.Complex.Cardinality
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.FieldTheory.Tower
 import Mathlib.Algebra.CharP.Invertible
@@ -472,3 +472,24 @@ theorem imaginaryPart_smul (z : ℂ) (a : A) : ℑ (z • a) = z.re • ℑ a +
 #align imaginary_part_smul imaginaryPart_smul
 
 end RealImaginaryPart
+
+section Rational
+
+open Cardinal Module
+
+@[simp]
+lemma Real.rank_rat_real : Module.rank ℚ ℝ = continuum := by
+  refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real
+  simpa [mk_real] using aleph0_lt_continuum
+
+@[simp]
+lemma Complex.rank_rat_complex : Module.rank ℚ ℂ = continuum := by
+  refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans mk_complex
+  simpa using aleph0_lt_continuum
+
+/-- `ℂ` and `ℝ` are isomorphic as vector spaces over `ℚ`, or equivalently,
+as additive groups. -/
+theorem Complex.nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ) :=
+  LinearEquiv.nonempty_equiv_iff_rank_eq.mpr <| by simp
+
+end Rational

Mathlib/LinearAlgebra/Dimension.lean

@@ -935,6 +935,17 @@ theorem rank_eq_card_chooseBasisIndex : Module.rank K V = #(ChooseBasisIndex K V
   (chooseBasis K V).mk_eq_rank''.symm
 #align module.free.rank_eq_card_choose_basis_index Module.Free.rank_eq_card_chooseBasisIndex
 
+/-- The rank of a free module `V` over an infinite scalar ring `K` is the cardinality of `V`
+whenever `#R < #V`. -/
+lemma rank_eq_mk_of_infinite_lt [Infinite K] (h_lt : lift.{v} #K < lift.{u} #V) :
+    Module.rank K V = #V := by
+  have : Infinite V := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
+  have h : lift #V = lift #(ChooseBasisIndex K V →₀ K) := lift_mk_eq'.mpr ⟨(chooseBasis K V).repr⟩
+  simp only [mk_finsupp_lift_of_infinite', lift_id', ← rank_eq_card_chooseBasisIndex, lift_max,
+    lift_lift] at h
+  refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left
+  exact (lift_umax.{v, u}.symm ▸ h_lt).ne
+
 end Module.Free
 
 open Module.Free