finrank_real_complex_fact — Mathlib

English

If E is a finite-dimensional vector space over ℂ, then E is finite-dimensional over ℝ.

Русский

Если E конечномерное над полем ℂ, то E конечномерно над ℝ.

LaTeX

$$$\\\\forall E\\\\, [\\\\text{AddCommGroup } E] [\\\\text{Module }\\\\mathbb{C} E] [\\\\text{FiniteDimensional }\\\\mathbb{C} E],\\\\ FiniteDimensional \\\\mathbb{R} E$$$

Lean4

/-- `Fact` version of the dimension of `ℂ` over `ℝ`, locally useful in the definition of the
circle. -/
theorem finrank_real_complex_fact : Fact (finrank ℝ ℂ = 2) :=
  ⟨finrank_real_complex⟩

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