rank_real_complex

Mathlib.LinearAlgebra.Complex.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#Complex.rank_real_complex

English

The dimension of ℂ as a vector space over ℝ is 2.

Русский

Размерность ℂ как векторного пространства над ℝ равна 2.

LaTeX

$$$\\\\operatorname{rank}_{\\\\mathbb{R}}(\\\\mathbb{C}) = 2$$$

Lean4

@[simp]
theorem rank_real_complex : Module.rank ℝ ℂ = 2 := by simp [← finrank_eq_rank, finrank_real_complex]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru