finrank_real_complex_fact' — Mathlib

English

The real vector space dimension of the complex numbers is 2, i.e., finrank_R(C) = 1 + 1.

Русский

Рациональное размерное пространство комплексных чисел над множеством вещественных чисел равно 2, то есть finrank_R(C) = 1 + 1.

LaTeX

$$ finrank_{\mathbb{R}}(\mathbb{C}) = 1 + 1 $$

Lean4

/-- Local instance to help the typeclass system to figure out `1 + 1 = 2`. -/
theorem finrank_real_complex_fact' : Fact (finrank ℝ ℂ = 1 + 1) :=
  finrank_real_complex_fact

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