rank — Mathlib

English

The real finiteness dimension of the log-space of units equals the unit rank of K: finrank_R(logSpace K) = Rank(K).

Русский

Размерность пространства логарифмов единиц поля K равна рангу единиц поля: finrank_R(logSpace K) = Rank(K).

LaTeX

$$$\operatorname{finrank}_{\mathbb{R}}(\mathrm{logSpace}\,K) = \operatorname{rank} K$$$

Lean4

/-- The unit rank of the number field `K`, it is equal to `card (InfinitePlace K) - 1`. -/
def rank : ℕ :=
  Fintype.card (InfinitePlace K) - 1

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