rank_rat_complex — Mathlib

English

The dimension of ℂ over ℚ is the continuum: rank_ℚ(ℂ) = continuum.

Русский

Размерность ℂ над ℚ равна континууму: rank_ℚ(ℂ) = континуум.

LaTeX

$$$\\\\operatorname{rank}_{\\\\mathbb{Q}}(\\\\mathbb{C}) = \\\\mathfrak{c}$$$

Lean4

/-- `C` has an uncountable basis over `ℚ`. -/
@[simp, stacks 09G0]
theorem rank_rat_complex : Module.rank ℚ ℂ = continuum :=
  by
  refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex
  simpa using aleph0_lt_continuum

Похожие утверждения