finrank_real_complex — Mathlib

English

The complex numbers form a 2-dimensional vector space over the real numbers.

Русский

Комплексные числа образуют вещественное векторное пространство размерности 2.

LaTeX

$$$\\\\mathrm{finrank}_{\\\\mathbb{R}}(\\\\mathbb{C}) = 2$$$

Lean4

/-- `ℂ` is a finite extension of `ℝ` of degree 2, i.e `[ℂ : ℝ] = 2` -/
@[simp, stacks 09G4]
theorem finrank_real_complex : finrank ℝ ℂ = 2 := by rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]

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