rank_real_complex'

Mathlib.LinearAlgebra.Complex.FiniteDimensional

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

← MathLib Explorer

English

There is a fact that finrank ℝ ℂ = 2.

Русский

Существует факт, что finrank ℝ ℂ = 2.

LaTeX

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

Lean4

theorem rank_real_complex'.{u} : Cardinal.lift.{u} (Module.rank ℝ ℂ) = 2 := by
  rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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