rank_real_of_complex — Mathlib

English

For any E that is a ℂ-module, the real rank of E equals twice its complex rank: rank_R(E) = 2 · rank_ℂ(E).

Русский

Для любого модульного пространства E над ℂ отношение размерностей: rank_ℝ(E) = 2 · rank_ℂ(E).

LaTeX

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

Lean4

theorem rank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] : Module.rank ℝ E = 2 * Module.rank ℂ E :=
  Cardinal.lift_inj.{_, 0}.1 <|
    by
    rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
    simp only [Cardinal.lift_id']

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