finrank — Mathlib

English

The real dimension of the mixed space equals the degree of K over ℚ.

Русский

Выразимость смешанного пространства по размерности равна степенью расширения K над \mathbb{Q}.

LaTeX

$$finrank_{\mathbb{R}}(\mathrm{mixedSpace}(K)) = finrank_{\mathbb{Q}}(K).$$

Lean4

protected theorem finrank : finrank ℝ (euclidean.mixedSpace K) = finrank ℚ K := by
  rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]

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