finrank_le_two — Mathlib

English

Let K be an RCLike field. Then K has finite real dimension at most 2; in fact it is spanned by {1, i} over ℝ.

Русский

Пусть K — поле RCLike. Тогда K конечномерно над ℝ размерности не более 2; пространство порождается множеством {1, i} над ℝ.

LaTeX

$$$\\operatorname{finrank}_{\\mathbb{R}} K \\le 2$$$

Lean4

theorem finrank_le_two : Module.finrank ℝ K ≤ 2 :=
  Module.finrank_le_of_rank_le <| rank_le_two _

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