complexToReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) complexToReal (E : Type*) [AddCommGroup E] [Module ℂ E] [FiniteDimensional ℂ E] :
    FiniteDimensional ℝ E :=
  FiniteDimensional.trans ℝ ℂ E

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