finrank_real_of_complex — Mathlib

English

For any E that is a ℂ-module, finrank_ℝ(E) = 2 · finrank_ℂ(E).

Русский

Для любого E с модулем над ℂ: финерank_ℝ(E) = 2 · финерank_ℂ(E).

LaTeX

$$$\\\\mathrm{finrank}_{\\\\mathbb{R}}(E) = 2 \\\\cdot \\\\mathrm{finrank}_{\\\\mathbb{C}}(E)$$$

Lean4

theorem finrank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] :
    Module.finrank ℝ E = 2 * Module.finrank ℂ E := by
  rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]

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