rclike_to_real — Mathlib

English

If K is an RCLike field, then K is finite-dimensional as a real vector space, spanned by {1, i}. In particular, dim_R K = 2.

Русский

Если K — поле RCLike, то K конечномерно над ℝ и порождается над ℝ множеством {1, i}; следовательно, dim_R K = 2.

LaTeX

$$$\\dim_{\\mathbb{R}} K = 2 \\quad\\text{and}\\quad K = \\operatorname{span}_{\\mathbb{R}}\\{1,i\\}$$$

Lean4

/-- An `RCLike` field is finite-dimensional over `ℝ`, since it is spanned by `{1, I}`. -/
instance rclike_to_real : FiniteDimensional ℝ K :=
  ⟨{ 1, I }, by simp [span_one_I]⟩

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