nonempty_linearEquiv_real — Mathlib

English

There exists a nontrivial linear equivalence between ℂ and ℝ as vector spaces over ℚ.

Русский

Существует линейное эквивалентное отображение между ℂ и ℝ как векторными пространствами над ℚ.

LaTeX

$$$\\\\exists e : (\\\\mathbb{C} \\\\simeq_{\\\\mathbb{Q}} \\\\mathbb{R})$$$

Lean4

/-- `ℂ` and `ℝ` are isomorphic as vector spaces over `ℚ`, or equivalently,
as additive groups. -/
theorem nonempty_linearEquiv_real : Nonempty (ℂ ≃ₗ[ℚ] ℝ) :=
  LinearEquiv.nonempty_equiv_iff_rank_eq.mpr <| by simp

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